Reasoning about Functional Programs and Complexity Classes Associated with Type Disciplines

We present a method of reasoning directly about functional programs in Second-Order Logic, based on the use of explicit second-order definitions for inductively defined data-types. Termination becomes a special case of correct typing. The formula-as-type analogy known from Proof Theory, when applied to this formalism, yields λ-expressions representing objects of inductively defined types, as well as λ-expressions representing functions between such types. A proof that a functional closed expression e is of type T maps into a λ-expression representing (the value of) e; and a proof that a function f is correctly typed maps into a λ-expression representing f (modulo the representations of objects of those types). When applied to integers and to numeric functions the mapping yields Church's numerals and the traditional function representations over them. The λ-expressions obtained under the isomorphism are typed (in the Second-Order Lambda Calculus). This implies that, for functions defined over inductively defined types, the property of being proved everywhere-defined in Second-Order Logic is equivalent to the property of being representable in the Second-Order Lambda Calculus. Extensions and refinements of this result lead to other characterizations of complexity classes by type disciplines. For example, log-space functions over finite structures are precisely the functions over finite-structures definable by λ-pairing-expressions in a predicative version of the Second-Order Lambda Calculus.

Authors

• Daniel Leivant

Keywords

• Calculus
• Arithmetic
• Logic programming
• Equations
• Computer science
• Binary trees
• Reasoning about programs
• Computer languages
• Power generation
• Functional Class
• Complex Class
• Isomorphism
• Representation Of Function
• Inference Rules
• First-order Logic
• Recursive Equation
• Finite Structure
• Reduction In Alpha
• Pairing
• General Types
• General Integration
• Computational Theory
• Free Variables
• Recursive Function
• Order Logic
• Universal Quantifier