Reading Lambda Calculus

Complex expressions in lambda calculus notation here is hard to parse in the head correctly until the day I started using Dart Language and noticed the connection between => lambda notation and C-style function layout. Here’s what I learned:

  • The expressions are right-associative because the right-most expression is the deepest nested function
  • Function application (feeding values to the arguments) always starts from left-to-right because you can only gain entry to a nest of functions starting from the outermost level, peeling it layer by later like an onion. So if applying arg to statement is denoted by (statement arg), the order of input would be (((statement arg1) arg2) arg3)
  • Names showing up on the parameter list of the nearest layer sticks to it (local to the function) and excludes everybody else (variable shadowing): this means the same name have absolutely no bearing as a free variable or being a free variable anywhere, so you can (and should) replace it with a unique name.

Here’s the calculus syntax in the book:

This example is the function application used above


Here’s where reusing the variable x in multiple places to mean different things gets confusing as hell, and the author (as well as the nomenclature) do not emphasize the equivalence to variable shadowing rules:

This can be rewritten as having

  • \lambda w . w^2
  • \lambda z . (z+1)
  • \lambda f . \lambda g . \lambda x.(f (g x) )

Upon application,

((\lambda f . \lambda g . \lambda x.(f \quad (g  \quad x) ) \qquad \lambda w . w^2) \qquad \lambda z . (z+1))

\implies (\lambda g . \lambda x.(\lambda w . w^2 \qquad (g \quad x) ) \qquad \lambda z . (z+1))

\implies \lambda x.(\lambda w . w^2 \qquad (\lambda z . (z+1) \quad x) )

which clearly reads for an input of x, it’ll be incremented first then squared. Resolving further:

\implies \lambda x.(\lambda w . w^2 \quad (x+1) )

\implies \lambda x.(x+1)^2

Fucking evils of variable shadowing! Not only it makes the code hard to read and reason, it also make the mathematics hard to follow!

Loading

Subscribe
Notify of
guest
0 Comments
Inline Feedbacks
View all comments