Curry-Howard-Lambek correspondence

From HaskellWiki

Revision as of 03:32, 2 November 2006 (edit) Uchchwhash (Talk | contribs) ← Previous diff		Revision as of 04:16, 2 November 2006 (edit) (undo) Uchchwhash (Talk | contribs) (more to come) Next diff →
Line 12:		Line 12:
	A (non-trivial) Haskell function takes maps a value (of type <hask>a</hask>, say) to another value (of type <hask>b</hask>), therefore, ''given'' a value of type <hask>a</hask> (a proof of <hask>a</hask>), it ''constructs'' a value of type <hask>b</hask> (so the proof its ''transformed'' into a proof of <hask>b</hask>)! So <hask>b</hask> is inhibited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering).		A (non-trivial) Haskell function takes maps a value (of type <hask>a</hask>, say) to another value (of type <hask>b</hask>), therefore, ''given'' a value of type <hask>a</hask> (a proof of <hask>a</hask>), it ''constructs'' a value of type <hask>b</hask> (so the proof its ''transformed'' into a proof of <hask>b</hask>)! So <hask>b</hask> is inhibited if <hask>a</hask> is, and a proof of <hask>a -> b</hask> is established (hence the notation, in case you were wondering).
	<haskell>toInteger :: Boolean -> Integer		<haskell>toInteger :: Boolean -> Integer
-	toInteger False = 0	+	inZ_2 False = 0
-	toInteger True = 1</haskell>	+	inZ_2 True = 1</haskell>
	says, for example, if <hask>Boolean</hask> is inhibited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery).		says, for example, if <hask>Boolean</hask> is inhibited, so is <hask>Integer</hask> (well, the point here is demonstration, not discovery).
		+
		+	== Connectives ==
		+	Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives <math>\and</math> and <math>\or</math>, though heavily disguised.
		+	Haskell handles <math>\or</math> conjuction in the manner described by Intuitionistic Logic. When a program has type <math>a \or b</math>, the value returned itself indicates its type.
	== Theorems for free! ==		== Theorems for free! ==

---

Revision as of 04:16, 2 November 2006

Curry-Howard Isomorphism is an isomorphism between types (in programming languages) and propositions (in logic). Interestingly, the isomorphism maps programs (functions in Haskell) to (constructive) proofs (and vice versa).

Contents 1 The Answer 2 Inference 3 Connectives 4 Theorems for free!

1 The Answer

As is well established by now,

The logical interpretation of the program is that the type is inhibited (by the value ), so the existence of this program proves the proposition (a type without any value is the "bottom" type, a proposition with no proof).

2 Inference

A (non-trivial) Haskell function takes maps a value (of type , say) to another value (of type ), therefore, given a value of type (a proof of ), it constructs a value of type (so the proof its transformed into a proof of )! So is inhibited if is, and a proof of is established (hence the notation, in case you were wondering). says, for example, if is inhibited, so is (well, the point here is demonstration, not discovery).

3 Connectives

Of course, atomic propositions contribute little towards knowledge, and the Haskell type system incorporates the logical connectives and , though heavily disguised. Haskell handles conjuction in the manner described by Intuitionistic Logic. When a program has type , the value returned itself indicates its type.

4 Theorems for free!

Things get interesting when polymorphism comes in. The composition operator in Haskell proves a very simple theorem.

The type is, actually, , to be a bit verbose, which says, logically speaking, for all propositions and , if from , can be proven, and if from , can be proven, then from , can be proven (the program says how to go about proving: just compose the given proofs!)