Discharging sub-derivations: A proof-theoretic Curry-Howard correspondence for a λ-calculus with patterns

Abstract From the perspective of the Curry-Howard correspondence (CH), abstraction over a variable in the simply-typed λ-calculus λ-calculus TAλ [3]corresponds to the proof-theoretic no-tion of discharge of an assumption in implication-introduction within natural-deduction (ND) proof-systems. Various (propositional) logics and λ-calculi can be obtained by side-conditions on the dis-charge/abstraction (see, e.g., [2] for side-conditions on the number of occurrences of the free abstracted variable in the body of the expression). Similarly, application in the λ-calculus corresponds by CH to implication-elimination in ND. In [4], a distinction is made between specific and non-specific assumptions. The former are introduced in an ND proof/derivation “according to their meanings”, while the latter are mere “placeholders ” (for a closed proof). While [4] focuses on differences in introducing the two kinds of assumptions, the current paper focuses on differences in the discharge of the two kinds. In the standard (simply-typed) λ-calculus, abstraction is based on non-specific assumptions. The term λx.M does not impose any restrictions on the “role ” of x within M. This view is corroborated by the standard β-reduction, that allows the (capture fee) substitution of an arbitrary term N for x in M, as the result of applying λx.M to N