Following the simple syntax we describe what it means to evaluate an <Expression>.
This method is sometimes called ‘eager evaluation’ or ‘call by value’.
This is the shortest precise description I know; it is a ‘big-step’ semantics and closely follows the program logic.
The green text below refers to identifiers in the C code and can be ignored for understanding the semantics.
The semantics is defined by explaining how a λ-expression is evaluated.
Such an evaluation always takes place in the context of ‘the current environ’ which is a construct env that binds values val to <ident>s (variables).
Environs are immutable and are generated as the program runs.
They continue to occupy space except in the ref-count version.
The <Expression> made available to the REPL is evaluated in the primal environ which makes these bindings.
There are two sorts of values which are functions:
- functions created upon evaluating an expression (λ<ident><Expression>).
Such a value is composed of:
- The <Expression>, called the body of the function, with some free variables,
- The <ident>
- An environ which provides a value for each free variable of <Expression> except <ident>.
- primordial functions:
- functions H and K exist in the form above but exist before any evaluations begin.
- Functions i, d, z and P are implemented in ad-hoc C code as part of the interpreter.
The value of an <Expression> which is an <ident> is the value that the current environ binds to that <ident>.
The value of an <Expression> which is (λ<ident>1<Expression>1) is a function whose body is <Expression>1, whose <ident> is <ident>1, and whose environ is the current environ.
To evaluate an <Expression> which is (<Expression>1<Expression>2)
both expressions are evaluated in the current environ and then it is required that the first value be a function which is automatic in the pure calculus for there are no other values.
A new environ is constructed which binds the <ident> of the function to the value of <Expression>2;
and other <ident>s are bound as they are in the environ of the function.
Then the body of the function is evaluated in this new environ.
That value of the body becomes the value of the original <Expression>.
Internals of an Environ
When a new environ is created it is implemented as the new value together with a pointer to the environ that was current when the evaluation occurred.
The environ is thus in fact a chain of bindings.
The environ chain that is current for expression x is exactly as long as there are λ subexpressions of the entire program which include x, plus the number or primordial functions.
Indeed the compiled <ident> is merely the number of steps required to step down the chain; this number is known at compile time.
The unit of dynamic allocation is thus the type env which includes new value and pointer to older env.
Other Notions of Evaluation
Lazy evaluation proceeds only by making note of what values might be needed and doing the evaluation only as they are demanded, ultimately by the requirement to print a result.
I do not know a precise definition of lazy evaluation.