| <!-- |
| Copyright (c) 2026 Ahmad Ali Parr. All rights reserved. |
| SPDX-License-Identifier: LicenseRef-Proprietary |
| Public source visibility does not grant an open-source license. See LICENSE. |
| --> |
|
|
| # Handwritten lambda-calculus proofs: pure SKI fragment |
|
|
| Application associates to the left. Bound variables are alpha-renamed to avoid |
| capture. The implementation uses de Bruijn indices for bound variables and |
| separate free atoms; see `idris/LambdaProofs.idr`. |
|
|
| ## Identity |
|
|
| `I = λa.a` |
|
|
| `I x = (λa.a) x →β x`. |
|
|
| Idris witness: `iBeta`, one `Contract`. |
|
|
| ## Constant |
|
|
| `K = λa.λb.a` |
|
|
| `K x y = ((λa.λb.a) x) y →β (λb.x) y →β x`. |
|
|
| Idris witness: `kBeta`, two contractions, the first inside the function position. |
|
|
| ## Substitution |
|
|
| `S = λa.λb.λc.(a c) (b c)` |
|
|
| `S x y z = (((λa.λb.λc.(a c) (b c)) x) y) z` |
|
|
| `→β ((λb.λc.(x c) (b c)) y) z` |
|
|
| `→β (λc.(x c) (y c)) z` |
|
|
| `→β (x z) (y z)`. |
|
|
| Idris witness: `sBeta`, three explicit contractions. |
|
|
| ## Scope and remaining obligations |
|
|
| The Idris witnesses quantify over symbolic free atoms. They do not yet establish |
| substitution lemmas for arbitrary compound operands, confluence, or operational |
| equivalence of the ATS evaluator. Unlambda is strict and effectful: beta equality |
| of pure SKI terms alone cannot justify reordering output, input, delay, or |
| continuation operations. |
|
|
| SPARK verifies Ada heap safety and contracts. It does not check these lambda |
| proof terms or the Idris compiler. The production argument additionally needs |
| ATS-to-model simulation, a checked FFI contract, and correspondence evidence for |
| the Idris heap abstraction and the concrete Ada implementation. |
|
|
