thhube/lambda-ineterpreter

A simple lambda calculus interpreter written in scala

A simple λ-calculus interpreter

A simple implementation of a λ-calculus interpreter. At current moment it uses rewrite as method for solving β-reductions also CAM(Categorical Abstract Machine) is available through option --cam<\code>.

To call the compiler: scala it.unipd.math.lambda.Main[--cam] filename
To use interactive shell: scala it.unipd.math.lambda.LambdaShell

Basic Usage

Lambda calculus basically has only variables, applications and lambda abstractions. To simplify language parse you have to write this way:

• [var, term] to write a lambda abstraction of kind λvar.term;
• (a, b) to applicate a to b - a(b);
• just declare variables and they will be allocated.

This is pure λ-calculus. There are just lambda terms and their beta reduction. Do not expect to have more than this. This interpreter has been done only for academic purpose.

lambda-ineterpreter's Issues

Lambda-rewiter fail

(a, ([x, x], (a, y))) fails to be normalized, is should go to a(a(y))

Omega is normalized

We should not normalize omega.

([x, (x, x)], [x, (x, x)])

becomes x(lambda x.x(x))

CAM environment enhance

Improve CAM, let user give the environment.