How do fixed-point combinators recursive constructions end up?

Question

Fixed-point compilers provide anonymous functions with the ability to refer to themselves or create 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.

In addition, fixed-point combinators can do recursive constructions, such as left-recursive grammar parsers. Consider Lickman 1995 , which proves the cessation of its implementation, but doesn’t actually mention how it works (this is just a phased conclusion from lattice theory to a haskell implementation) and why it needs fixed-point compilers in a language that already supports recursion initially.

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

Answer 1

From a quick scan, at the end of 5.3, Lickman writes: "As defined above, fixS provides sufficient performance on all continuous inputs."

The point is to force the fixed-point operator to produce enough output so that the parsing continues. You cannot do this for a general fix :: (a -> a) -> a , but specializing from a to Set a or later Parser a to get enough structure (namely a lattice) to work.

Again, I just looked at the thesis, but I believe that the proof (in section 5.5) of the statement “ h :: Parser a -> Parser a supports the performance property ==> fixP h is productive” is key.

Answer 2

Of course. Here is a simple correct recursive grammar in three rules:

 S -> b T T -> a S T -> a 

These three rules allow you to build a parser to recognize these strings:

 type Parser = String -> (Bool, String) s :: Parser s "" = (False, "") s (c : cs) = if c == 'b' then t cs else (False, cs) t :: Parser t "" = (False, "") t (c : cs) | c == 'a' && cs == "" = (True, "") | c /= 'a' = (False, cs) | otherwise = s cs 

If you want to do a more general parsing, just select Bool so that there is some kind of data structure instead, perhaps stored in Maybe to indicate a failure. Returning (False, ___) on unsuccessful analysis will help if S has some other rules, for example, for example. S -> TT and T -> bb . Then, when we get "b" followed by (False, ___), we rewind to try S -> TT . These types of grammars can be performed with a little lubrication and elbow recursion.

The three rules above will successfully match strings like "ba", "baba", etc. We could also write these lines left recursively, like:

 S -> T a T -> S b T -> b 

What happens if you try to write the same parsers above? Endless loop if you look at the front of the line. The problem is that the function S will first call the function T, and then T will first call S, and they will mutually recursively count infinity. The computer is not smart enough to know that postconditions (“followed by a”, “followed by a”) make further decisions impossible; he simply descends into your functions and hopes that you know what you are doing.

How does a good fixed-point combinator help? Well, think of these rules as a description of a tree: then the evaluation of the function crosses this depth of the tree, and this particular tree is infinite in that direction. On the other hand, a walk around the width can be based on these rules and can raise a result that uses the smallest of these functions, and this is the "least fixed point" for a particular function based on this grammar. So, why the correct fixed-point combinator (based either on diag in the article or on the combinator of lattice theory) may stop when describing these rules, while naive recursion will not.