Jon Awbrey
Registered: Feb 2004
Posts: 551 |
Propositions As Types
The topic known as the "propositions as types analogy" (PAT)
or the "Curry-Howard Isomorphism" (CHI) has just come up on
another thread, so I am going to drop a nominal anchor here
as a way to remind me to get back to it later when I return
from a short holiday.
The PAT analogy is commonly summed up in the mnemonic form:
"Proofs are to Propositions as Terms are to Types".
Very roughly, it states that there is a correspondence between
the propositions of a particular ("intuitionistic") variant of
propositional calculus and the types of functions in a certain
brand of functional calculus. What's more, the correspondence
is such that the constructive existence of a term t of a given
type T, a fact that one writes as "t : T", affords a blueprint
for constructing a proof p of the corresponding proposition P.
Jon Awbrey
Last edited by Jon Awbrey on 06-21-2004 at 12:24 PM
Report this post to a moderator | IP: Logged
|
04-20-2004 05:34 PM
