Home » forums » LtU Forum

Curry/Howard and Disjunction

Whilst tralling for Propositions-as-Types references a question arose about the difference between disjunction in propositional logic calculi and sum-types in PLs.

To the best of my knowledge Curry/Howard makes a connection between the 2 concepts even though disjunction is an inclusive-or and sum-types are exclusive, e.g.

A v B ~= A | B | A x B

Am I missing something?

Is choice disjunction in CL also exclusive?

By Daniel Slaney at 2005-11-02 14:10 | LtU Forum | previous forum topic | next forum topic | other blogs | 5907 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Think of a proof term (ie, a

Think of a proof term (ie, a lambda term) as a witness that you have sufficient evidence to demonstrate that the proposition (ie, the type) is provable.

In this sense, you can make an A + B if you've got an e1:A, an e2:B, or both. In the case where you've got evidence for both A and B on hand, you can prove A + B two different ways, either with inl e1 or inr e2, whichever you like.

By neelk at Wed, 2005-11-02 14:38 | login or register to post comments

Both sum type former and logical disjunction are inclusive or

The sum type described in CH is inclusive sum.

By Charles Stewart at Wed, 2005-11-02 16:48 | login or register to post comments