The Curry-Howard Correspondence

The Curry-Howard Correspondence reveals a close correspondence between the constituents of Logic and of Programming. Also known as the Formulas as Types and the Proofs as Programs interpretations.

Existential Quantification (∃) of Logic corresponds to the Generalized Cartesian Product type (∑) of Programming. Universal Quantification (∀) of Logic corresponds to the Generalized Function Space type (∏) of Programming. Conjunction (⋀) of Logic corresponds to the Product type (×) of Programming. Disjunction (⋁) of Logic corresponds to the Sum type (+) of Programming.

There are associations between the Curry-Howard Correspondence and the fourfolds of the Square of Opposition, Attraction and Repulsion, and of course Linear Logic.

http://en.wikipedia.org/wiki/Curry-Howard_correspondence

<>

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s


%d bloggers like this: