/lox

Untyped λ-calculus interpreter

Primary LanguageCommon Lisp

λox the lambda-calculus interpreter

Features

Parser

λox uses parsnip, the monadic parser combinator library (and they say you need a Haskell to parse things!) to parse input stream into terms of following types:

  • variable (symbol): x,
  • abstraction (λ-function): λx.M,
  • application: M N.

Application is left-associative, i.e. terms are applied by pairs from left to right:

LOX> (lox-parser:parse-term "a b c d")
(((a b) c) d)

Order could be altered by using parenthesis as one would do in regular mathematical expressions:

LOX> (lox-parser:parse-term "a b (c d)")
((a b) (c d))

Example — fixed-point combinator definition:

LOX> (lox-parser:parse-term "λf.(λx.f (x x)) λx.f (x x)")
λf.(λx.(f (x x)) λx.(f (x x)))

Evaluator

TODO. I don’t want to do the fun part alone… waiting for my friends to find some spare time.

Reduction

De Bruijn indexes should be assigned to all variables to avoid name collisions and simplify α-reduction.

Numbers

It’s not decided yet whether Lisp’s numbers should be included in the interpreter. It’s possible to encode natural numbers using Church encoding, after all.

IO

Lololol

Global Scope

I am thinking of introducing the walrus operator (:=) for defining global variables. This is a way of making λox behave more like the general-purpose programming languages, i.e. you can define functions and libraries and namespaces… except everything’s lambda.