This is an interpreter for the Untyped Lambda Calculus and (if wanted) System F-Omega. The typed mode can (in the future lol) be enabled at your option.
- Untyped Lambda Calculus (base).
- Extension that allows native naturals.
- Extension that allows native booleans.
The Untyped Lambda Calculus is the base of the interpreter. It's a minimalistic and simple way to represent computation.
The interpreter allows for native naturals, so you can define and use them using standard digits. Digits are not enabled when this extension is disabled.
They provide function to operate over those native types. When applied with other abstractions, they simply cannot Beta-reduce.
The informal grammar of this language is as follows:
Expression :=
| TermVariable -- Variable (initial lowercase).
| Lambda TermVariable "->" Expression -- Abstraction.
| Expression Expression -- Application.
| "(" Expression ")"
Declaration :=
| "let" TermVariable ":=" Expression "." Declaration*
| EndOfInput
Expression application is left-associative and has the highest precedence. Parentheses are used to indicate precedence, and abstraction binds the most.
As prompt: id id id id someFreeVar
As context:
let id := \x -> x.
The prompt only allows Expressions, and the context only allows Declarations.
Only the frontend web (Scala JS) is working. That is:
mill -w lambda.fullLinkJS
# or
mill -w lambda.fastLinkJS
But tests run on the JVM:
mill -w lambdaCoreJVM.tests
We should have a JVM/LLVM frontend in the near future.
- System F-Omega.