9/12/2019
The basic grammar for Lambda expressions is:
<expression> := <variable> | <function> | <application>
<function> := λ<variable>.<scope>
<application> := (<function expression> <argument expression>)
<scope>:= <expression>
<function expression>:= <expression>
<argument expression>:= <expression>
<variable>:= any string of characters (excepting ( λ . )) starting with a lower case letter
Later this will be extended by adding:
<expression> := <defined constant>
<defined constant>:= any string of characters (excepting ( λ . )) starting with an upper case letter
Here are some examples.
Three lambda expressions which are variables are 'a', 'aVariable', and 'firstVar'. In other logical systems, often there is talk of constants and variables. That distinction is not really made here, at this stage, all these basic terms are thought of as variables. Later we are going to augment these variables with certain other defined terms such as the numerals '0', '1' -- these defined terms are constants
Three lambda expressions which are applications are '(a b)', '(myFunction myArgument)', and '(fun arg)'. Conceptually, applications are the application of a function to an argument, just as, in trigonometry, '(cos 30)' is the application of the cosine function to the value 30, in the lambda calculus, '(a b)' is the application of the function 'a' to the value 'b'. With an application there is a space between the function and its argument, thus '(f g)'. A remark here, function application is a 'silent' operator (it is so silent it does not exist at all). It is infix binary and left associative, so if we were to use @ to signify it, a sample expression might be ((f@g)@h).
Three lambda expressions which are abstractions, or anonymous functions, or lambdas, are 'λx. b', 'λm.(p q)', and 'λa. λb. b'. Abstractions have the form λ<variable>.<expression>, often it is convenient to identify the right hand expression part after the period as being the 'scope' of the abstraction. [You may be familiar with this notion from predicate logic, where there is talk of the 'scope' of quantifiers.]
Some other systems use juxtaposition to mean application, so 'ab' means 'a@b'. This is fine except that it requires that variables have length one so that we know that 'ab' is two variables juxtaposed not one variable of length 2. But we want to labels like 'firstVariable' to mean a single variable, so we cannot use this juxtaposition convention.
It is not easy to get your eye in with lambda expressions. You can try a few here.
[The lambda symbol λ is hard to produce from a keyboard. There are two solutions: there is a symbol palette under the Omega ('symbol') button,or the parser will accept the Haskell convention of permitting the backslash \ as a substitute for λ (this is illustrated below).]
Functions of several variables are mimicked in the lambda calculus by means of 'currying' (from Haskell B. Curry, though apparently due to Schoenfinkel) and the ability of the lambda calculus to return functions. For a clear example let us suppose that the lambda calculus had in it the primitive addition operation, then λx.λy.(+ x y) would be the counterpart of two variable addition, but this function would be applied one argument at a time so λx.λy.(+ x y) applied to 3 would return λy.(+ 3 y) which is itself a function, and when this returned function was applied to, say, 2 (+3 2) would be returned. Thus multivariable functions are simulated by cascaded single variable functions.