Search code examples
parsinghaskellrecursioncompiler-constructioncombinators

How can fixed-point combinators make recursive constructs terminate?


Fixed-point combinators provide a way for anonymous functions to refer to themselves or to build mutually recursive structures. Although useful in lambda-calculus, they are essentially superfluous in modern programming languages because most if not all support recursion, lambdas and closures.

Also, fixed-point combinators can make recursive constructs like left-recursive grammar parsers terminate. Consider Lickman 1995, who proves termination for his implementation but never actually mentions how it works (it's just a step-by-step derivation from lattice theory to the haskell implementation) and why he needs fixed-point combinators in a language that already supports recursion natively.

How does it work and why does he require a fixed-point combinator?


Solution

  • From a quick scan, at the end of 5.3, Lickman writes "As defined above, fixS is ensured to been sufficiently productive on all continuous inputs."

    The point is to get the fixpoint operator to produce enough output so that parsing can continue. You can't do that for a general fix :: (a -> a) -> a but specializing a to Set a, or later Parser a, gives enough structure (namely that of a lattice) to work with.

    Again, I've just looked through the thesis cursorily, but I think the proof (in section 5.5) of the statement "h :: Parser a -> Parser a maintains the property of productivity ==> fixP h is productive" is key.