Notation (skip this if you wish)

There are widely differing conventions for notation. Let me explain what the problems are and some of the suggestions. We have to capture three types of thing... variables, abstractions, and applications and the problem is that many even quite simple expressions will contain lots of these. So if brackets are used, say with applications and abstractions, there will be lots of them or a bracket omitting convention will be needed coupled with left or right associativity.

Ideas:- In mathematics round brackets get used for function application, thus f(3), h(3+2). Quite often, too, in maths the brackets are left out and function application is indicated merely by juxtaposition eg cos 30. Juxtaposition is also used in LISP, although the whole application is surrounded by brackets eg (COS 30).In logic, there are quantifiers and these and their scope are picked out by brackets eg ∀x(<scope>) or (∀x.<scope>) and, in some senses, an abstraction using lambda is just a new kind of quantifier expression, so these conventions could be used.

Thus, in long form

λx((f(g))(h))

now leave some brackets out by using juxtaposition for application and associate function application to the left (to fit in with Currying) so f g h means (f(g))h)

λx(f g h)

we can go slightly further than this by letting quantifiers run as far right as possible so our expression becomes

λx.f g h

the dot is used to separate out the binding variable from the rest.

Also, many writers use variables of length 1. If this is done, the space between expressions (partly to signify application) can be left out, thus

λx.fgh which means λx.f g h which means λx((f g) h)

THIS IS MORE OR LESS THE STANDARD AND MOST COMMON CONVENTION.

Church, Barendregt, and others typically defined lambda expressions with brackets around both applications and abstractions (and they don't use a period in the basic grammar). Then they adopt a bracket omitting convention, which both uses a period and which allows them to leave out brackets. The problem with this, for us, is that we are going to use some software to parse expressions. If the period is not part of the grammar the parser is not going to parse it. So we prefer to have the period in, and to have few brackets in the basic expressions.

Mathematica, a great system, uses square brackets for function application eg cos[30]. (We would love to use this. The problem is that students doing supplementary reading would have difficulty matching up these notes, in Mathematica formalism, and their readings.)

Revesz has a suggestion, which seems very sensible (yet very non-standard). It is merely to include the function part of an application in brackets (ie instead of writing f 3 or f(3) or f[3] you write (f) 3)! This, in one hit, makes the grammar LL(1), which means it can be parsed without lookahead, and clears all problems. The left bracket then becomes the prefix operator 'apply'.

Revesz grammar:-

<l-expression> ::= <variable>| <application>|<abstraction>
<application>::= (<l-expression>) <l-expression>
<abstraction>::= λ<variable>.<l-expression>

and a typical expression looks like (λx.x) y

Another argument or motivation that Revesz offers is that maths is intrinsically applicative order so f(x) means work out x first then apply f to it. In functional systems (ie the lambda systems) we prefer normal order evaluation so we should write (f)x to mean work out f first then apply it to x. (What normal order and applicative order evaluation mean will be explained later.)

Anyway, I'm all in favour of Revesz, but for the time being we'll muddle along with what we have.

We want variables to be able to have more than one letter in them; for example, we'd like 'firstArg', 'secondArg', etc. to be able to be single variables. This means that any juxtaposition to indicate application has to use something like a space as a separator. So, for example, 'firstArg' is a single variable, whereas 'f i r s t A r g' may be something like '((((f i) r) s) etc.. A similar consideration applies to lambda abstractions. We need to be able to distinguish between 'λfirstVar' where 'firstVar' is the variable and 'λf   irstVar' where 'f', alone is the variable and 'irstVar' is something to do with the scope. This distinction can be made using a period, thus 'λfirstVar.' and 'λf.irstVar'.

This gives us a proto-grammer that looks like this:-

<expression> ::= <variable>| <application>|<abstraction>
<application>::= <expression> <expression>
<abstraction>::= λ<variable>.<expression>

Then there is one final modification to make. If we put applications within brackets, first of all we will be able to parse the expressions unambiguously, but then also it assists with the visual spotting of beta reductions. Beta reductions, which we will learn about later, require, first of all, an application, and then they require a lambda abstraction as the left hand expression. These means they start '(λ'. The opening left bracket indicates an application and the λ in position two indicates that the left expression of the application is an abstraction. This is very useful to know. So our grammar is

Grammar :-

<expression> ::= <variable>| <application>|<abstraction>
<application>::= (<expression> <expression>)
<abstraction>::= λ<variable>.<expression>

With our conventions, all brackets are mandated, none can be omitted and you cannot use extra ones for disambiguation (there is no need to disambiguate for nothing is ambiguous). Roughly speaking, most normal approaches use twice as many brackets (for they bracket around abstractions) and then they have conventions for omitting brackets. We use half the number of brackets but everything has to be there. Our main motivations here are clarity for students coupled with the ability of software to read and parse the expressions easily.