Nice article, definitely piqued my interest in the lambda calculus, but there were a few points that were confusing for me as my first glimpse at the lambda calculus.
The first confusing point was the lack of definition of the order of operations. I first stumbled at the line (λy.(λx. x) y) a b . Is this supposed to be (λy.(λx. x) y) (a b) or ((λy.(λx. x) y) a) b . In this case both give the same answer, but it's not obvious that associativity holds in general.
It gets worse with the Y combinator: λf. (λx. f (x x))(λx. f (x x)) . Is this (λf. (λx. f (x x)))(λx. f (x x)) or λf. ((λx. f (x x))(λx. f (x x))) . Peeking ahead, it seems to be the latter, which makes more sense (otherwise the letter f would be pressed into service in two different contexts), but it's totally ambiguous from the rules that have been presented in the article.
The other point of confusion was regarding rule #3 (If t and s are both valid λ-terms, then t s is a valid λ-term.) The article tells is a certain manipulation we can do if t is a "function" (i.e. something that begins with a λ, I don't know the technical name for this), but doesn't say what to do if t is not a "function". As far as I can tell the answer is: do nothing, there is no simplification in this case. It would be nice if this was said explicitly.
There are only two bits of syntax for lambda calculus: 'application', written "a b", and 'abstraction', which I'll write as "\a. b" (since "\" is easier to type than lambda). The words "abstraction" and "function" are pretty-much interchangable, although we might use "abstraction" to specifically refer to a "new" function definition, like this:
\x. x
As opposed to a "calculated" function, like the result of an application:
a b
Regarding precedence, application is "left-associative", meaning that
a b c
is the same as
(a b) c
Abstractions 'capture' everything after the ".", so
\a. b c \d. \e. f
is the same as
\a. (b c \d. (\e. f))
You need to use parentheses to go the other way, eg.
a (b c)
(\x. x) y
In the case of the Y combinator, there is only one "f" variable but it gets used twice. There are two "x" variables, one per abstraction, although those abstractions just-so-happen to look the same. In other words, we could replace one of the "x" abstractions with "\y. f (y y)" (known as an "alpha conversion") but we can't rename one of the "f"s without renaming all three occurences.
Regarding your last point, the only semantic values in lambda calculus are functions, so "t" can't be anything else. However, we just saw that there are two syntactic forms which "t" can take. If "t" is an abstraction, we can simplify our expression immediately via the beta-reduction rule ('applying t to s').
If "t" is an application, like "t1 t2", then we can try simplifying that to get either an abstraction (which we can apply to "s") or another application, which we can try simplifying, and so on.
It's possible (due to the Halting Problem) that we keep getting applications no matter how much we try to simplify, in which case we've hit an infinite loop while trying to calculate "t", and hence we can never reach the point where we can apply it to "s".
>It's possible (due to the Halting Problem) that we keep getting applications no matter how much we try to simplify, in which case we've hit an infinite loop while trying to calculate "t", and hence we can never reach the point where we can apply it to "s".
But note that the _order_ of the reductions doesn't matter, as long as they're valid reductions. We always get the same result or it never halts like you said.
This interview with Robert Wilson is totally bonkers: https://youtu.be/sKFVorIvpAo?si=LbfQFK8-7OziqyUI&t=1322