Source language \(λ_{AL}\)

Base terms

Grammar for base terms

The type of base terms. (Figure 1 in paper.)

• "Var x" represents "\(x\)".
• "Def f x t" represents "\({\bf let }\; y = f\, x \;{\bf in }\; t\)".
• "DefTuple [x₁; ...; xₙ]" represents "\({\bf let }\; y = (x₁, ..., xₙ) \;{\bf in }\; t\)".

Syntactic sugar

In the paper, we write @(f, x) for let y = f x in y where y is chosen sufficiently fresh. Notice that Var (Idx O) is an adequate implementation for y.

Change terms

Grammar for change terms

Change variables are represented by DeBruijn indices.

The type of change terms. (Figure 1 in paper.)

• "dVar x" represents "\(dx\)".
• "dDef f x dt" represents "\({\bf let}\; y = f\, x, dy = df\, x\, dx\, {\bf in}\, dt\)".
• "dDefTuple [dx₁; ...; dxₙ] dt" represents "\({\bf let}\; y = (x₁, ..., xₙ), dy = (dx₁, ..., dxₙ) \, {\bf in}\, dt\)".

Notice that we could have used the same syntax as term to represent change terms since they are totally isomorphic. Yet, we prefer a form of "strong" typing in the formalization to avoid any confusion in the definitions, in particular in the operational semantics, in the program transformation and the validity relation.

Basic syntax mechanisms

Read as "un-d", undo d, not German und.