File size: 1,635 Bytes
d8df231 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 | <!--
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.
|