The relational lambda calculus is the computational syntax that the relationality derivation produces at step 10 (Terms), when the relational field’s self-referential and compositional structure hardens into manipulable expressions.
In standard mathematics, a typed lambda calculus is a formal system of variables, abstraction (function formation), and application, governed by a type discipline that guarantees well-behavedness. The simply typed lambda calculus, System F, and the calculus of constructions are progressively more expressive variants. See standard treatments of type theory for the conventional development.
What distinguishes the relational lambda calculus is that its syntax, types, and evaluation properties are all derived rather than stipulated. The derivation reaches it through the following forced sequence:
- The relational field has self-reference (through Reflexive Sequence) and sequential composition (through Composition). The capacity for self-reference within sequential structure forces Term — a position that refers to something within a context.
- Term differentiates into three forms: Variable (a named position), Function (a body that binds a variable and returns a result), and Application (a function meeting an argument).
- Self-application — a function applied to itself — produces Fixed Point: a term whose evaluation yields itself.
- Application simplifies through Reduction, terminating in Value (an irreducible term).
The type discipline is not imposed from outside. Judgements (step 11) assign properties to terms within contexts, and the Heyting algebra (step 12) organizes those judgements into a constructive logic. This algebra constrains the syntax through three properties: Soundness (well-typed terms do not go wrong), Confluence (different reduction paths reach the same result), and Normalization (every term reaches a value).
The relational lambda calculus is the computational layer on which the later formal structures operate. Flow and Nucleus act on the field of terms and judgements; Observation witnesses values; Profiles reconstruct the full syntax internally.