I'll give this a whirl. Meanwhile, I've briefly looked into introductory articles on Lambda Calculus on more than one occasion, and I'm always left wondering if it would benefit from a more readable notation. Here's an example:
I realize that LC is of interest to CS folks who probably think in code fragments that look a lot like this, but for someone like me, the notation gets pretty impenetrable, pretty quick.
As I understand it, a number of developments in science and math (calculus, newtonian mechanics, maybe even algebra) remained the domain of philosophers until someone came up with a teachable notation.
> I realize that LC is of interest to CS folks who probably think in code fragments that look a lot like this
LC is code. It is a minimalist programming language. The notation is mature and has been around for decades. I don't think there are shortcuts for this, you need to spend time to get accustomed to the syntax, which is the easy part. But you can always use different syntax if you want to. For instance LISP or ML like, there are even graphical notations but I don't think it'll make things easier.
In any case, you usually don't need to write complex terms. Terms can be denoted by symbols and complex things are defined iteratively. For instance, after you defined church numerals, you can call them 0,1,2,3....
Besides, the meta theory doesn't require to write tons of terms anyway. For instance, things like proofs of church rosser property, strong normalization of simply typed lambda calculus and so on.
However, it's true that some students get scared away by the notation. When it looks too much like maths, they run away. But make them play with Scheme and it suddenly much easier!
Actually, in my opinion, the beauty of the LC is that it connects maths and programming. Things like semantics, type checking, compilation, interpretation, reduction strategy, all can be defined formally on this minimal yet turing complete language. And conversely, various logics can be defined using typed lambda calculus (see Curry Howard isomorphism).
Thanks. I'm not scared by math, but might just need to write things down myself so I can space out the formulas. I never learned math just by reading, so I suppose that I shouldn't expect to do so with LC. Part of this could be my crappy eyesight.
> I never learned math just by reading, so I suppose that I shouldn't expect to do so with LC.
Yes, and I think that's the problem nowadays with internet learning. We go through a lot of resources, picking up things here and there. And we don't take the necessary time to write things down and solve exercises.
With the lambda calculus, I think you eventually need to write terms and perform the reductions. A fun thing to do is to play with fixed point combinators. It's really not difficult, just take a little patience and discipline.
One problem is simply that the notation is linear, while lambda calculus is inherently hierarchical. That problem affects all programming languages to some degree, but it is particularly damaging to the comprehension of lambda terms.
Another problem is the complications that are introduced by giving names to variables. This has actually been discussed quite a bit in literature.
For example, that the term "λx.xx" is alpha equivalent to "λy.yy", simply means that the language has redundancy. In fact "alpha equivalence", "unbound variables", and "capture avoiding substitution", are all concepts made necessary by the use of names. If you refuse to name terms, the calculus becomes conceptually simpler. This isn't a revalation by any means. Church pointed this out. It just happens that naming things is a very useful thing to do when writing proofs. So we kind of just have to deal with it.
Point-free reasoning is a good way to avoid some of these complications, which contributes to the popularity of combinator calculi like SKI when teaching untyped lambda calculus.
Another way is to use a graphical representation to depict variable binding more explicitly. See examples below:
Actually, now that I'm reading the term, I'm a little surprised by the notation λsz.s(z).
I think it is more conventionally written λsz.s z (and similarly in ML: fun s z -> s z).
If you write it without syntax simplification, it is (λs.(λz.(s z))). Then, you usually write only one lambda as it can be seen as function with two arguments (λsz.(s z)). Then you remove the most outside parenthesis: λsz.(s z). Since abstraction has lower precedence that application, you can finally write it λsz.s z.
An important thing to know is that in functional langages (lambda calculus, lisp or ML), application is written (f x) - and not f(x) - and is left associative, so (f x) y is written f x y.
I agree, working out the grouping and precedence in the equation you posted has always been what's tripped me up. Like you, I've tried to understand on several occassions, for several years. In my case, I've never had anyone to ask. Even in college (third tier state school) none of the CS professors were familiar with lambda calculus.
Nicely done! This document is short enough to not cause mental overload and yet explains the most important aspects in a comprehensible way.
Too many “tutorials” read like complete gibberish to the people they're supposed to address, namely beginners (try understanding `camlp4`, e.g.). This one doesn't make that mistake.
It's meant more in the sense you might hear "the ring of the integers" or "the field of complex numbers". The lambda calculus is a calculus (i.e., one of many.) "Which calculus? The lambda calculus."
You might not hear "the algebra" very often, but you might talk about an algebra, and if the particular algebra you're talking about is clear from context you might sometimes refer to it as "the algebra".
In this sense I think the word "calculus" tends to mean "formal system".
Sure, PDFs are anything but painless. I need a reader to look at them. Many of my devices don't have one or have some off brand one. Esp since I don't want to be beholden to the adobe update process.
I see. On most platforms, you should be able to get some PDF reader, open-source or otherwise. You could even use your browser. And seriously, what doc format could you look at without a “reader”?
“painless” was obviously meant with reference to the document's contents, not its representation format.
Whatever your reasons for disliking PDFs are, you can't expect an author to pander to every possible idiosyncrasy of the audience.
S1 ≡ (λwyx.y(wyx))(λsz.s(z)) = λyx.y((λsz.s(z))yx) = λyx.y(y(x)) ≡ 2
I realize that LC is of interest to CS folks who probably think in code fragments that look a lot like this, but for someone like me, the notation gets pretty impenetrable, pretty quick.
As I understand it, a number of developments in science and math (calculus, newtonian mechanics, maybe even algebra) remained the domain of philosophers until someone came up with a teachable notation.