Curry-Howard isomorphism

The Curry-Howard isomorphism (also known as the Curry-Howard correspondence ) is the interpretation of types as logical statements and of terms of a certain type as proofs of the statement belonging to the type; and vice versa. It is named after the mathematicians Haskell Brooks Curry and William Alvin Howard .

Semi-formal description

The concept of truth is exchanged with the concept of provability , thus follows the intuitionist understanding of mathematics. A statement is provable if there is a term that has the type that matches the statement.

Simple joiners

A proof of conjunction is a pair of proofs for both and . ${\displaystyle A\land B}$ ${\displaystyle (p,q):A\times B}$ ${\displaystyle A}$ ${\displaystyle B}$

Evidence of a disjunction is a term from the disjoint union of and , . ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle A+B}$

Evidence for implications is total functions of the type . ${\displaystyle A\to B}$ ${\displaystyle A\to B}$

The logical negation is usually defined as an abbreviation for , where under the Curry-Howard isomorphism corresponds to the empty type . ${\displaystyle \lnot A}$ ${\displaystyle A\to \bot }$ ${\displaystyle \bot }$

Quantifiers

A universally quantified statement becomes a function where the type of function value depends on the value of the function argument. So here you meet dependent types . ${\displaystyle \forall {a\in A}:{X(a)}}$

The proof of an existentially quantified proposition must yield two things: an element , and a proof for . ${\displaystyle \exists {a\in A}:{X(a)}}$ ${\displaystyle A}$ ${\displaystyle a}$ ${\displaystyle X(a)}$

Evidence example

The theorem of the excluded third usually does not apply in constructive logic calculi (if it were valid, every statement would be decidable, which leads to either weakness of expression or inconsistency ). A version with double negation below the universal quantization via statements can, however, be proven by specifying a proof term. We are looking for a proof for any statements ${\displaystyle A}$

${\displaystyle \lnot \lnot (A\lor \lnot A)}$,

which under Curry-Howard and with the dissolution of the negation abbreviation a term of type

${\displaystyle ((A+(A\to \bot ))\to \bot )\to \bot }$

becomes. The lambda expression

${\displaystyle \lambda f.f(\kappa _{2}(\lambda a.f(\kappa _{1}a)))}$

represents a term of the desired type, where and the injections are in the two-digit sum type. ${\displaystyle \kappa _{1}\colon A\to (A+(A\to \bot ))}$ ${\displaystyle \kappa _{2}\colon (A\to \bot )\to (A+(A\to \bot ))}$

Practical applications

Available and usable evidence assistants / programming languages ​​such as Coq , Epigram, and Agda make use of the Curry-Howard isomorphism by allowing evidence to be specified as programs and statements as types. The type verifier takes on the task of verifying the specified evidence.

swell

• Simon Thompson: Type Theory and Functional Programming (PDF; 1.3 MB)
• Bengt Nordström, Kent Petersson, Jan M. Smith: Programming in Martin-Löfs Type Theory (PDF; 709 kB)
• Philip Wadler: Propositions as Types (PDF; 261 kB)