It's a good question, if we consider that it's been unanswered on the computer science stack exchange for four years. https://cs.stackexchange.com/questions/83533/practical-usage...

Basically, it does beta normal form reduction. In these kinds of situations, I sometimes feel like it's just as valuable to know how to get the darn thing to run, and then the rest explains itself. So for the purposes of this explanation, I'll share a Hello World example for this interpreter, that should hopefully get you going. This won't cover beta reduction or any of that jazz. Just the simplest possible usage that you can type into the web page at https://crypto.stanford.edu/~blynn/lambda/ and see something happen.

(\a.(\b.a(b b))(\b.a(b b)))(\a.\b.b(\c.c)(\c.\d.a c(a d))(\c.\d.a(c d)))(\a.\b.\c.c(\d.\e.\f.\g.e d))
# a.k.a. Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))
# a.k.a. [[Y λλ [[[0 λ 0] λλ [[3 1] [3 0]]] λλ [3 [1 0]]]] λλλ [0 λλλλ [2 3]]]

It should spit out the identity function:

λd.d

Why did this happen? It's because Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd))) is the reducer a.k.a. E and λabc.c(λdefg.ed) is the argument. What is λabc.c(λdefg.ed)? It's an encoded version of the identity function λd.d. So in other words, all it did was output exactly what was inputted. Except the input had to be encoded. Why is it encoded? Normally in LISP, if we wanted to pass a program to a self-interpreter, we've wrap the argument in (QUOTE), e.g.

(EVAL (QUOTE (LAMBDA (X) X)))

However the lambda calculus doesn't have a QUOTE builtin. Because the lambda calculus is a programming language that has only has a single keyword (can you guess what it is?) What they had to do instead was design a system of quoting that only uses lambdas:

Var=\m.\a b c.a m
App=\m n.\a b c.b m n
Lam=\f.\a b c.c f

Or if you prefer SectorLambda notation:

var="λλλλ [2 3]"
app="λλλλλ [[1 4] 3]"
lam="λλλλ [0 3]"

So if you want to derive the argument yourself, you can type the following into the Stanford web page.

Lam (\y.Var y)
=> λa b c.c(λy a b c.a y)

You can even use the self-interpreter with SectorLambda. https://justine.lol/lambda/ For instance, the behavior of the reduced output will be the same as if you just typed in the normal identity function:

{ printf %s 'Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))' | lam2bin.com; printf '0101'; } | blc; echo
0101
{ printf %s 'λa.a' | lam2bin.com; printf '0101'; } | blc; echo
0101

Another fun exercise, if you want to see all the steps that take place in reducing the self-interpreter, would be to download the lambda.com and lam2bin.com programs, and run the following command:

printf %s 'Y(λab.b(λc.c)(λcd.ac(ad))(λcd.a(cd)))(λabc.c(λdefg.ed))' | lam2bin.com | lambda.com -vl
Y (λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d))) (λabc.c (λdefg.e d))
λa.a ⍆ Y (λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d))) (λabc.c (λdefg.e d)) ⋯
a ⍆
a=(Y (λbc.c (λd.d) (λde.b d(b e)) (λde.b(d e))) (λbcd.d (λefgh.f e)) ⋯)
Y λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) λabc.c (λdefg.e d) ⋯ ⍆
λb.a(b b) λb.a(b b) λabc.c (λdefg.e d) ⋯ ⍆
a=λbc.(c (λd.d) (λde.b d(b e)) (λde.b(d e)))
a b b λabc.c (λdefg.e d) ⋯ ⍆
b=λc.(b(c c))
a=λbc.(c (λd.d) (λde.b d(b e)) (λde.b(d e)))
λab.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) b b λabc.c (λdefg.e d) ⋯ ⍆
λb.b (λc.c) (λcd.a c(a d)) (λcd.a(c d)) λabc.c (λdefg.e d) ⋯ ⍆
...

Hope this helps!

See also https://web.archive.org/web/20180714080803/http://repository...