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

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