Is My Lambda Calculus Unique?

Question

I am trying to write a small compiler for a language that processes lambda calculus. Here is the ambiguous definition of the language I found:

E → ^ v . E | EE | ( E ) | v 

Symbols ^,., (,) And v are tokens. ^ represents lambda, and v represents a variable. An expression of the form ^ vE is the definition of a function, where v is the formal parameter of the function, and E is its body. If f and g are lambda expressions, then the lambda expression fg is an application of the function f to the argument g.

I am trying to write an unambiguous grammar for this language under the assumption that the function application remains associative, for example, fgh = (fg) h, and this function application is bound more tightly than., For example, (^ x. ^ Y. Xy) ^ zz = (^ x. (^ y. xy)) ^ zz

Here is what I have, but I'm not sure if this is correct:

 E -> ^vE | T T -> vF | (E) E F -> v | epsilon 

Can anyone help?

Answer 1

Between reading your question and comments, you seem to be looking more for help in learning and implementing lambda calculus, not just the specific question you asked here. If so, then I am on the same path, so I will share some useful information.

The best book I have that cannot be said is the best book possible, Types and Programming Languages ( WorldCat ) by Benjamin K. Pearce. I know that the name is not like lambda calculus, but take a look at λ-Calculus extensions: the meaning of extension characters , which lists many of the lambda calculus that come from the book. There is code for the book in OCaml and F # .

Try searching CiteSeerX for research in lambda calculus to find out more.

The best λ-calculus evaluator I've found so far:

A tool for recovering lambda calculus with information here .

In addition, I find that you get much better answers to lambda calculus questions related to CS: StackExchange programming and math related questions in Math :. Stackexcahnge

As for programming languages ​​for implementing lambda calculus, you probably need to learn a functional language if you haven't; Yes, this is a different beast, but the enlightenment on the other side of the mountain is impressive. Most of the source code that I find uses a functional language such as ML or OCaml, and once you learn it, the rest becomes easier to learn.

To be more specific, here is the source code for the project of untyped lambda calculus, here is the input file for changing F # YACC, which, after reading the previous questions , seems to be in your world of knowledge and here is an example of input.

Since the grammar is designed to implement REPL, it starts at the top level, thinks of the command line and accepts several commands, which in this case are expressions of the lambda calculus. Since this grammar is used for many calculi, it has parts that are the place holders in earlier examples, so the link here is more about the place.

Finally, we will move on to the part that you after

Note. LCID is a lowercase identifier

 Term : AppTerm | LAMBDA LCID DOT Term | LAMBDA USCORE DOT Term AppTerm : ATerm | AppTerm ATerm /* Atomic terms are ones that never require extra parentheses */ ATerm : LPAREN Term RPAREN | LCID 

Answer 2

You can find evidence of a certain ambiguity of the grammar in sublinear time, but to prove that the grammar is unambiguous is the complete NP task. You will need to generate all possible sentences in the language and verify that for each of them there is only one conclusion.