"Types are propositions. Programs are demonstrations" (Haskell Curry).
Curry-Howard Correspondence
The Curry-Howard correspondence (or isomorphism) −by its proponents, the logicians Haskell Curry and William Alvin Howard− is considered one of the great discoveries in logic. It is based on a surprisingly simple idea but with profound consequences for the relationship between logic and computer science:
To a type A of elements corresponds the logical proposition Ap "A is inhabited" or "A is not empty".
An element of type A is a demonstration of proposition Ap, for if the type A is not empty, then the proposition Ap is true.
For example, if int is the type of integers, the associated proposition is intp "integers are inhabited". If 3 is an integer, then this number is the demonstration of the proposition intp. If a programming language has integers, that is, if it has type int, then intp is V (true) and F (false) if it does not.
Once we have logical propositions associated with types, it is possible to define compound propositions (with logical operators) based on types:
Implication.
If we have a function f with an argument of type A and producing as result an element of type B, then the function f is of type A→ B, i.e., to each element of type A corresponds an element of type B.
To this type of function corresponds the implication Ap→ Bp, where Ap is "A is inhabited" and Bp is "B is inhabited". This implication means that if A is inhabited, then B is also inhabited. If A is inhabited, there is an element a of type A and there is also an element of type B, which is f(a). Therefore, B is inhabited and Bp is V. In short, given an element of type A], there is a demonstration of Ap, and the function f] constructs an element of type B and a demonstration of Bp.
Conjunction.
If we have two types, A and B and the corresponding propositions Ap and Bp, the conjunction of these two propositions is Bp∧ Ap. This conjunction is V if Ap and Bp are both V. For their demonstration we need a demonstration of Ap and of Bp. An element that includes both demonstrations is a pair of elements (a, b), where a is an element of type A, and b is an element of type B<. The pair (a, b) is an element of the Cartesian product C of the sets formed by the elements of type A and those of type B, respectively. A conjunction demonstration is thus an element of C.
Disjunction.
If we have two types, A and B and the corresponding propositions Ap and Bp, the disjunction of these two propositions is Ap∨ Bp. This disjunction is V if Ap or Bp is V. For its proof we need a proof of Ap or of Bp. An element that includes one of the two demonstrations is an element that belongs to the union D] of the sets associated with types A and those of type B, respectively. A disjunction demonstration is an element of D.
Negation.
The negation of the proposition Ap "A is. inhabited" is Ap' "A is not inhabited".
Given the established correspondence between types and propositions, the notation is usually unified: a type A is equivalent to the proposition A. Therefore:
A→B is both a type and a proposition. If A→B] is an inhabited type, the proposition A→B is a theorem.
An implication A→B] can be considered a program (or a type of function) where A is the input type and B is the output type. The output is the demonstration of the implication. Application and implication are dual to each other.
If A×B is an inhabited type, the proposition A∧B is a theorem. Conjunction is a type of Cartesian product.
If A∪B is an inhabited type, the proposition A∨B is a theorem. Disjunction is a type resulting from a union of types.
A program that performs a proof has some input types (corresponding to propositions) and an output type (corresponding to the proposition to be proved).
To prove a logical theorem T, all we have to do is construct a type t based on the input types (which are axioms) that reflects the structure of the theorem, and then find an element that has that type t. Examples of logical theorems are
A → AA] → B → AA∧B → A (A∧B → C) ↔ (A → B → C)
The inverse Curry-Howard correspondence −hence an isomorphism− is:
To each proposition corresponds a type. If the proposition is true, its type is V. If the proposition is false, its type is F. This is equivalent to the Fregean concepts of "sense" and "reference", where the proposition is the sense and the truth value its reference.
The Curry-Howard correspondence connects:
Types with propositions. In general, types with logical formulas.
Logic and programming languages with propositional logic, two previously unrelated areas.
The static (logic) with the dynamic (computation).
Demonstrations and programs. The way of proving logical theorems (universally true propositions) is standardized by means of programs. Programs are demonstrations of logical theorems. Demonstrations, when represented by programs, can be automated.
The Curry-Howard correspondence and the unification between logic and computer science
It all started in 1934, when Haskell Curry interpreted the type as a proposition and an element of the type as a proof of the proposition. In 1958, Curry concluded that types made it possible to express intuitionistic logic.
Intuitionistic logic is a type of logic that is constructive. A proof of A→B] is an algorithm that computes B from A. To prove a theorem it is sufficient to supply an example that satisfies the theorem. It does not follow the law of the excluded third (a proposition is V or F).
Later, William Alvin Howard discovered that a large number of intuitionistic logics could also be expressed, including higher-order intuitionistic logic. In 1969, Howard discovered a formal analogy between the programs of the lambda calculus and the proofs of natural deduction.
Natural deduction is an approach to demonstration theory in which one seeks to emulate the way people reason when performing mathematical demonstrations. Instead of using several axioms to which a few rules of inference apply, natural deduction proposes to consider as few axioms as possible and to extend the number of rules of inference by introducing two rules for each logical operator (one to introduce it and one to eliminate it). Natural deduction was introduced by Gerhard Gentzen in his work "Investigations on logical inference", published in 1934-35. Since the discovery of the Curry-Howard correspondence, natural deduction has gained significant importance as a foundation for computer science (especially for functional programming), since its formulation corresponds to the lambda calculus. [see Applications - Logic - Natural Deduction]].
The Curry-Howard correspondence has been the driving force behind a large spectrum of new research. In particular, it has led to a new class of formal systems that can act both as proof systems and as programming languages. This field of research is often referred to as "modern type theory". It has even been speculated that the Curry-Howard correspondence could be instrumental in achieving a common foundation for mathematical logic and computer science.
Specification in MENTAL
First, we must differentiate between class and type:
A class is a set of elements that share a property.
Type in computer science is an intrinsic property that the elements of a class have.
A property can be intrinsic (the one denoted by the element itself) or extrinsic (associated from outside the element). An extrinsic property is also called an attribute or predicate.
]
If x is an element of a class C and its corresponding type is t, the property is satisfied:
⟨( x/t ↔ x∈C )⟩ x/t reads "x is t" or "x has property t"
x/t indicates that x] is of type t
For example, if we have that D={0...9} is the set of all digits, and we call d its corresponding type, we have the conditional equivalence
(⟨ x/d ↔ x∈D )⟩
In the Curry-Howard correspondence, if an element is of type t, that implies the proposition t≠∅ (t is inhabited or t is not empty). In MENTAL, if an element x is of type t], x/t and ((x/t)? = α) are satisfied.
In MENTAL we have the following features:
There is no need to interpret the type as a proposition, since both are expressions. Therefore, the Curry-Howard correspondence is not necessary because it is implicit in the language.
There is equivalence between type and predicate: if x has predicate t, x is of type t. For example,
"Pepe is man" is represented as Pepe/man. Pepe has the predicate man and Pepe is a type of man.
"3 is an integer" is represented as 3/integer. 3 is a type of integer and has the predicate integer.
"3 is a digit" is represented as 3/d. 3 is a type of d (digit) and has the predicate d.
The universal type (or universal expression) is α, which corresponds to the predicate "exists" and replaces the logical formula or proposition V (true). The null type (or null expression) is θ, which corresponds to the predicate "does not exist" and replaces the logical formula F (false). These universal programming types are the same as the logical types, i.e. logical types and programming types are unified. They are the same.
Demonstrations are constructions and are not bound to the dual concept V-F. There are no truth values, but existential values (existence and non-existence), which are the real logical values that serve for decisions and implications. Truth is treated as a qualitative magnitude, of the form f*V. Truth is a predicate, e.g., x/V or x/(0.7*V).
Types can be combined by means of primitives, like any other expression, and therefore there can be higher-order types, parameterized types, computed types, interleaved types, virtual types, etc. Behind the types is all the power of the language to create new types.
In Curry-Howard correspondence, programs are demonstrations. In MENTAL, programs are also demonstrations, which are constructions realized by instances of the semantic axioms.
The property is satisfied.
⟨( x/A → y/B → (x→y)/(A→B) )⟩.
That is, if x is of type A and y is of type B, then x→y is of type A→B. Analogously for conjunction and disjunction:
⟨( x/A → y/B → (x∧y)/(A∧B) )⟩
⟨( x/A → y/B → (x∨y)/(A∨B) )⟩
MENTAL and logical unification - computer science
Since the time of Gödel, Curry, Church, Turing, Shannon and von Neumann, the foundations of computer science have been intrinsically linked to mathematics, especially mathematical logic. This historical link was reinforced by the discovery of the Curry-Howard correspondence, which provided a direct connection between two disciplines: programming and formal logic.
However, this link has not been considered sufficient, as it was desired to achieve a complete isomorphism between programming and classical logic. Three main alternatives were tried. Some authors started from programming, selecting particular characteristics, as a foundation and tried to adapt classical logic to a type system. Other authors chose the opposite path: they chose logic as the foundation and tried to derive new programming paradigms, fields or concepts. Finally, a third group focused on the search for a common middle ground between programming and logic.
In essence, the problems were twofold: 1) how to do computations with logic; 2) how to do logic with computation.
MENTAL provides a very simple answer to these problems. The answer is simply to transcend logic and computation, so that the connection between computation and logic is made, not at the horizontal level, but at the vertical or deep level: through the primary archetypes:
Logic is based on the primitive "Condition", which is used for decision logic. Together with a generic expression it enables the logic of deduction or inference.
The "particularization" primitive is used to specify both types and predicates. A "type" is simply a type of predicate.
Logic and computer science cannot be unified because they are distinct disciplines, but both have the same common foundation: universal semantic primitives, as do propositional logic or predicate logic.
Thus, it is not necessary to look for a computational content to classical logic.
Bibliography
Griffin, T.G. Formulae-as-types notion of control. In Conf. Record 17th annual ACM Symposium on Principles of Programming Languages, POPL’90, pp. 47–58. ACM Press, 1990.
Howard, William Alvin. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, 1980.
Krebbers, Robbert. Clasical logic, control calculi and data types. Master´s Thesis. October 2010. Internet.
Poernomo, Iman; Crossley, John N.; Wirsing, Martin. Adapting Proofs-as-Programs. The Curry--Howard Protocol. Springer, 2010.
Sheard, Tim. Putting Curry-Howard to Work. Internet.
Simmons, H. Derivation and Computation. Taking the Curry-Howard correspondence seriously. Cambridge University Press, 2000.
Sorensen, M.H. Lectures on the Curry-Howard Isomorphism. Elsevier Science, 2006.
