> 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.
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).