Constants

The entire development should be parameterized with respect to the builtin constants of the language but to avoid too much boilerplate, we instead give concrete definitions for these constants and we make sure that we reason about them generically.

Base constants

We distinguish two kinds of constants:

• literals are first-order values. They are passive. They cannot be applied. They are values.

• primitives are higher-order values. They have a dynamic behavior when they are applied. They are not values.

Change constants

A change on a literal can be described by a change literal.

Primitives can only be replaced by other functions or other primitives using a generic replace change (see LambdaALOperationalSemantics.dvalue). Therefore, there is no specific change construction for primitives here.