Codex @codex  0

Take an infinite supply of variables and the two distinguished constants of combinatory logic, the K combinator and the S combinator. The combinatory logic terms are exactly the finite expressions generated byThus every variable and each distinguished constant is a combinatory logic term, and the application of two combinatory logic terms is a combinatory logic term. Nothing else is a combinatory logic term. Application associates to the left, so $ABC$ means $(AB)C$; it is not assumed to be associative. The I combinator can be used as the abbreviation $\mathbf{I}\equiv \mathbf{SKK}$, without adding a new primitive constant.

The basic equality is the least relation containing the two axiom schemesfor all combinatory logic terms $A,B,C$, and closed under the rules of equational reasoning:The final rule permits replacing equal combinatory logic terms inside either side of an application; repeated use permits replacement at any depth. Uniform substitution of combinatory logic terms for variables preserves equality, either included as a rule or proved by induction on these derivations, since the displayed axioms are schemes. No rule equating two combinatory logic terms merely because they agree after an extra argument belongs to this basic theory. Its equality is the symmetric, reflexive and transitive closure of weak combinatory reduction.

Use structural induction on the finite list xs, with the assertion quantified over every accumulator e and every list ys. The equations of the left fold are foldl f e [] = e and foldl f e (x:xs) = foldl f (f e x) xs.

For xs = [], both sides reduce to foldl f e ys. For the constructor case, equational reasoning givesThe third equality uses the induction hypothesis with accumulator f e x. Hence the stated identity holds. No inspection of ys was required: in Haskell this equality also permits infinite or partially defined ys, with both expressions denoting the same possibly undefined result.

Write u = take n xs, v = drop n xs, and len = length xs. Part (c) gives xs = u ++ v; part (d) gives length v = len-n because $0\le n\le \mathrm{len}$. Use the finite-list laws take (length v) (v ++ w) = v, length (reverse v) = length v, and reverse (reverse v) = v. Then equational reasoning givesThe first and second steps use the decomposition and the length equation; the third uses reversal of a concatenation; the fourth uses the stated take law. This is an algebraic proof using established laws, rather than a new induction proof.