The algebraic λ-calculus is a conservative extension of the ordinary λ-calculus

05/01/2023
by   Axel Kerinec, et al.
0

The algebraic λ-calculus is an extension of the ordinary λ-calculus with linear combinations of terms. We establish that two ordinary λ-terms are equivalent in the algebraic λ-calculus iff they are β-equal. Although this result was originally stated in the early 2000's (in the setting of Ehrhard and Regnier's differential λ-calculus), the previously proposed proofs were wrong: we explain why previous approaches failed and develop a new proof technique to establish conservativity.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset