(C) Ralf Lämmel, Andrei Varanovich, University of Koblenz Landau

Logistics

• Course site
• Date published: 28 Nov 2012
• Deadline SVN: 4 Dec 2012 (End of Day)
• SVN: https://svn.uni-koblenz.de/softlang/main/courses/plt1213/students + group name
• Present your solution with your own system.
• Lab assistant calls up teams.

Assignment

Prolog implementations of relevant lambda calculi are available here:

• Untyped lambda caclulus (the basic lambda calculus from the lecture)
• an applied lambda calculus (NB-like numbers and Booleans)

Another applied lambda calculus

The existing implementation of an applied lambda calculus essentially goes through some modularity trickery to extend NB into a lambda calculus with NB-like support for numbers and Booleans. Have a look at don't get lost in these levels of modular composition. Use it for inspiration, if you like.

Start from the code of the untyped lambda calculus and patch it to add Booleans (with and, or, negation) directly and Prolog numbers (with +,-,*,/) as well as comparison for numbers (==,<,>,<=,>=). Thus, numbers and comparisons are treated differently than in NB. Try to factor code well so that you don't have too much code cloning in the eval predicate for all these many operations. (Again, you don't have to use the same crazy, modular approach as mentioned above.)

Demonstrate your result with a demonstration of the factorial function. You will need to use a fixed point combinator. This one should do it:

lam(f,app(
            lam(x,app(var(f),lam(y,app(app(var(x),var(x)),var(y))))),
            lam(x,app(var(f),lam(y,app(app(var(x),var(x)),var(y)))))))

Prolog variables as lambda variables

Warning: you are entering the hacking corner of this course. If you handle this one, then you deserve a "hero badge" for this course, at least, the Prolog part thereof. Also, you will understand substitution in ways that make your life more meaningful.

The existing implementation of the lambda calculus uses Prolog atoms for the representation of lambda variables. Arguably, one might want to take advantage that Prolog readily implements substitution by representing lambda variables instead as Prolog variables. Revise the implementation accordingly. You will be able to kick out the implementation of substitution.

Important hint: you are quite likely to need a weapon like this to get the semantics of beta reduction operationally right: copy_term/2