💾 Archived View for soviet.circumlunar.space › ayb › lab › lambdaself.gmi captured on 2023-05-24 at 18:35:13. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Lambda Calculus self interpreter

This small post will describe a small self interpreter for untyped lambda calculus, it will be a function taking a lambda expression encoded in itself and output the beta reduced term. Though the document will allow a pretty standard syntax for expressions with the addition of multi-letter variables for the sake of readability.

First, we are going to need some basic data types and functions to work with them. Will use Scott encoding for convinient pattern matching.

True  = \x y.x
False = \x y.y
if c t f = c t f

Zero = \x y.x
Succ n = \x y. y n
eq n m = n (m True (\x.False)) (\n'.m False (\m'. eq n' m'))

Then we are going to encode lambda expressions, with De Bruijn indices in Scott encoing:

Var n   = \p _ _. p n
Abs b   = \_ p _.p b
App l r = \_ _ c.p l r

We will need, for our interpreter a helper function for substitutions:

substitution expr n repl =
  expr
    (\m -> if (eq n m) repl expr)
    (\b -> Abs (substitution b (Succ n) repl))
    (\l r -> App (substitution l n repl) (substitution r n repl))

We can, now, implement our eval function, which is based on beta reduction:

eval e =
  e
    (\v -> Var v)
    (\b -> Lam b)
    (\l r ->
      (eval l)
        (\v -> Var v)
        (\b -> substitution b Zero r)
        (\l r -> App l r))

And, here we are, we have a fully working self interpreter for a turing-complete language written in less than 10 minutes.