C[omp]ute

From: "andrew cooke" <andrew@...>

Date: Fri, 20 Jan 2006 12:03:14 -0300 (CLST)

This is related to the thread I had on AskMe -
http://ask.metafilter.com/mefi/29489

Since I've given up Mefi in disgust and sorrow, I thought I'd follow up
here with some links to related items on Wikipedia.

Curry-Howard correspondence (lots of interesting stuff here) -
http://en.wikipedia.org/wiki/Curry-Howard_correspondence - "the close
relationship between computer programs and mathematical proofs [...] There
are a number of ways to think about the Curry-Howard correspondence. In
one direction, it operates on the level compile proofs into programs. Here
proof was, originally, limited to proofs in constructive logic — typically
in a system of intuitionistic logic."

And another way to look at the excluded middle - Peirce's law -
http://en.wikipedia.org/wiki/Peirce's_law

Vaguely related - Heyting algebras -
http://en.wikipedia.org/wiki/Heyting_algebra - "... arise as models of
intuitionistic logic, a logic in which the law of excluded middle does not
in general hold"

Andrew