(ref.doc)lambda

Lambda Calculus:

p 130, 5.4 A formal definition of lambda notation
A lambda expression has one of the following three forms:
- An identifier, or *atom*
- lambda x . e, where x is an identifier and e a lambda expression;
  this form is called an *abstraction*
- f(e), where f and e are lambda expression; this form is called an
  *application*


Denotational Semantics:

p 150
The validity function defines the construct's static semantics;
validity functions are also called "context conditions" or
"constraints".
The meaning function gives the construct's dynamic semantics, or
*denotation*.

p 164
This requirement that *apply_binary* yield 'unknown* whenever one or
more of its arguments is *unknown* is a special case of a general
property called *strictness*. Here *apply_binary* is said to be strict
on both its arguments.

p 228, 8.1.3 Non-creativity
As opposed, for example, to an axiom, a definition should be
*non-creative* in the sense that any property expressible with *h* may
also be expressed without *h*, by replacing *h* with *D* throughout.