Revision as of 22:41, 22 July 2021

Lambda calculus – it's basic rules are unbelievably simple and it can compute anything and everything =

Lambda diagrams are a way to visualize lambda calculus.
Lambda calculus is an extremely simple formalism that is equally expressive to the (much more widely known) Turing machine.
That is: Lambda calculus is "Turing complete".
Any program that is in principle logically possible can be written in Lambda calculus.
A maximally universal computer. At least that is what is the current (2021) consensus on the topic.

The special thing about lambda calculus is that:
Lambda calculus is used very much unchanged as the core of a number of practical programming languages.
Perhaps more so than the Truing machine is.
("practical programming languages" meaning programming languages that are in use in practical applications to a quite notable degree.)

Graphical visualizations for lambda calculus

There are a number of graphical visualizations for Lambda calculus.
The most straightforward one is just to plot out the syntax tree.
There are only three types of elements in the syntax tree of lambda calculus:

• abstractions
• applications
• variables

It's as simple as that.
Well, adding evaluation strategies and a type system makes it a bit more complicated.
But that is the basic gist.

Plain lambda diagrams (PLDs)

An especially nice visualization for lambda calculus are (unannotated) "lambda diagrams".
These are presented by John Tromp on his homepage here: https://tromp.github.io/cl/diagrams.html

Annotated lambda diagrams (ALDs)

Adding some annotations to lambda diagrams may make these into an amazing programming interface with some awesome properties.
Smack in the middle of between textual and visual programming.
See main page: Annotated lambda diagrams

On the fundamentality of lambda calculus

Lambda calculus is without a doubt a very fundamental calculus.
There is no such things as the most fundamental calculus though.

• Unfortunately because we like to seek "perfect" solutions.
• Fortunately because we'll never run out of new "miracles".

Turing machine seems less fundamental

The equally expressive truing machine model with

• unboundedly long memory tape and
• finite table of rules

certainly seems less fundamental than the lambda calculus.
In that a concrete implementation of the model is less elegant and less amenable to mathematical handling.

"Overloading" lambda calculus

Lambda calculus can be abstracted over by an category theory based interpretation.
See: Compiling to categories (Conal Elliott)
It's kinda like overloading the meaning of function application and ...

Equivalent calculi

There are other calculi equivalent in expressiveness like e.g. the SKI calculus.
Maybe less intuitive though. While identical programs (same fixed points) can be represented, they differ in run-times.
(Interestingly conversion between calculi in general is a hard problem)

Similar but different calculi

There are other calculi that are similarly sparse in rules like e.g. the pi-calculus.
(wiki-TODO: Look into this again – is the property of mathematical substitutability given?)

Functional vs Relational

Lambda calculus is modelling functional relationships not relational relationsships.
There is a directionality in functional relationships while there is none in relational relationships.
Evaluation needs a direction to proceed so this kinda makes sense maybe?

Related

• Annotated lambda diagrams
• Annotated lambda diagram mockups
• Lambda diagrams
• Warning! you are moving into more speculative areas. – The program that constructs and executes all possible programs

External links

• Lambda calculus
• Turingmachine
• SKI combinator calculus, B, C, K, W system