ॐλ

I have forayed in to FP multiple times 1. However λ calculus is something I keep coming back to in various levels of detail.

The first time I looked at in seriousness was 2 which is the best introduction to λ calculus I have seen. However the syntax is often confusing and the details of evaluation are often intricate, since the theory itself is equational and doesn’t demand a specific order of reduction or evaluation. 3 does a great job of clarifying ambiguities. 4 provides explanations of various reduction (or evaluation if its fully fleshed out) schemes. 56 give the matrix of eager/lazy X shallow/deep = Weak Normal Form, Normal From, Weak Head Normal Form, Head Normal Form permutations of reduction strategies with results from the example. While trying to replicate the PL zoo from ML in scala, research in to Top down parsers that can be used showed up Parsley: 7. It turns out writing and using natural grammars and parsers that terminate are often different things:8 but that’s a deviation from the main exercise of theoretical computation systems.

⍵ or loop = (λ.x x x) (λ.x x x)

If Y given f, x is is written as f( f (x)) and x is substituted by f(x), we have recursion.

Y f x = f(f(f(.... (f(x))))

//  Y combinator
Y = λ.f (λ.x f (x x)) (λ.x f (x x))

=> λ.f (λ.x f ((λ.x f (x x)) (λ.x f (x x)))) 

=>  λ.f (λ.x f (f (λ.x f (x x)) (λ.x f (x x))))

=> λ.f (λ.x f (f (λ.x f ((λ.x f (x x)) (λ.x f (x x))))))

...

Y f x = f (f x)

I had encountered fixed points in compiler backend code - primarily to eliminate cycles in graphs and my forays in to FP 9. Also it is often mentioned that recursion can be converted to iteration for performance reasons - representing the FP and Imperative view of the same problem. It is interesting to know that a problem is considered computable if there’s a recursive algorithm for it.

While the methods to convert from recursion to iteration or vice-versa are somewhat known to programmers, the formal methods are often quite opaque. The most interesting part of the Y combinator in the context of λ calculus is that a simple language that does not support recursion is used to implement recursion. Conversely the notion of identifying fixed points in code is used in code with recursive types to extract a concrete type. More will be said in 1

While doing some research on lambda calculus (postfix) for a usecase I had, I chanced upon the De bruijn index: 1011

From which I translated the pun on Eke 12:

ಏಕೆ = [ [೧ (೦ ೦)] [೧ (೦ ೦)] ]

Eke = [ [1 (0 0)] [1 (0 0)] ]

In the standard form,

Y = λf. (λx. f (x x)) λx. f (x x)

can be written as:

ಏಕೆ = ॐಅ . (ॐಉ . ಅ (ಉ ಉ)) ॐಉ . ಅ (ಉ ಉ)

Eke = Om a . (Om u . a (u u)) Om u . a (u u)

Without any semantic change.

Haskell uses \ for λ and -> for .

Pretty cool to use as a basis for any generative language.

If that’s too abstract, see this 5 To see how easily program structure is derived from lambda calculus.

Some of this writeup was done in the context of trying to understand Tree Sitter 13 a VS code plugin that lets you do AST searches and highlights in your editor based on the grammar of a language of your choice. I was experimenting with a grammar for λ calculus since its a good starting point 14.

It’s very tempting to state that λ calculus is a great start for a small programming language. However it’s small but not easy to use as a direct programming language esp if you see how numbers are defined. To understand levels of expressivity: 15 was quite useful.

As we go up the expressive chain of λ calculus

  1. Untyped λ Calculus 16
  2. Simply Typed λ calculus 17
  3. System F 18
  4. System F⍵ 18

Alternate Computational Models 19 that come up are:

  1. SKI Calculus 20
  2. Iota and Jot 21
  3. Generalized Recursion 22
  4. Subleq 23

Full fledged fields of study:

  1. Predicate Logic 24
  2. Category Theory 25
  3. λ calculus 16
  4. Turing Machines 26

The equivalences between the above fields of study have been known since 27

28 29 provides a rosetta stone between Logic, Computation, Category Theory, Physics and Topology.

Benjamin Pierce’s classic books provide the best introduction to Type theory. 4 30 31 are great resources.

Category Theory can get pretty abstract for working programmers. I found Bartosz’s videos, blogs and book a good way to understand some basics 32 33

One recent experiment that was interesting was how it was shown that LLMs can act as a computer 34 and well summarized here 35.

  1. https://github.com/vwulf/ettuge/blob/master/src/main/md/pl/FP.md ↩ ↩2

  2. https://youtu.be/eis11j_iGMs?si=sM5lTjltqQrGGfPN ↩

  3. https://personal.utdallas.edu/~gupta/courses/apl/lambda.pdf ↩

  4. https://www.cis.upenn.edu/~bcpierce/tapl/ ↩ ↩2

  5. https://github.com/andrejbauer/plzoo/blob/master/src/lambda/example.lambda ↩ ↩2

  6. https://github.com/andrejbauer/plzoo/tree/master/src/lambda ↩

  7. https://github.com/j-mie6/parsley ↩

  8. https://youtu.be/RQ6UWMgHWtA?si=PNfnwl_c_GQG-gmv ↩

  9. https://www.youtube.com/watch?v=XHiTK4UOIf0 ↩

  10. https://loup-vaillant.fr/articles/programming-ring ↩

  11. https://dev.to/dannypsnl/de-bruijn-index-why-and-how-32f6 ↩

  12. https://github.com/vwulf/ettuge/blob/master/src/main/md/kannada/Eke.md ↩

  13. https://youtu.be/09-9LltqWLY?si=CJ1TbuAjvMGPwUX8 ↩

  14. https://cs.stackexchange.com/questions/109954/writing-a-grammar-for-lambda-calculus ↩

  15. https://www.youtube.com/watch?v=43XaZEn2aLc&list=PL1a1q1zrmyEwpA2PvYcM1UqE18zekujW-&index=17 ↩

  16. https://en.wikipedia.org/wiki/Lambda_calculus ↩ ↩2

  17. https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus ↩

  18. https://en.wikipedia.org/wiki/System_F ↩ ↩2

  19. https://en.wikipedia.org/wiki/Model_of_computation ↩

  20. https://en.wikipedia.org/wiki/SKI_combinator_calculus ↩

  21. https://en.wikipedia.org/wiki/Iota_and_Jot ↩

  22. https://en.wikipedia.org/wiki/General_recursive_function ↩

  23. https://en.wikipedia.org/wiki/One-instruction_set_computer ↩

  24. https://en.wikipedia.org/wiki/First-order_logic ↩

  25. https://en.wikipedia.org/wiki/Category_theory ↩

  26. https://en.wikipedia.org/wiki/Turing_machine ↩

  27. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence ↩

  28. https://drive.google.com/file/d/12-bpFUNpX0aI_aXEVPQNBhmJUJuZQf2O/view?usp=drive_link ↩

  29. https://arxiv.org/abs/0903.0340 ↩

  30. https://www.cis.upenn.edu/~bcpierce/attapl/ ↩

  31. https://www.cis.upenn.edu/~bcpierce/papers/books_bib.html#PIERCE91 ↩

  32. https://bartoszmilewski.com/ ↩

  33. https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_ ↩

  34. https://github.com/anadim/subleq-transformer/blob/main/round1_constructed/report.pdf ↩

  35. https://x.com/DimitrisPapail/status/2028669695344148946?s=20 ↩