Relational semantics

From LLWiki
Revision as of 21:47, 14 March 2009 by Thomas Ehrhard (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Relational semantics

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula A as a set A * and a proof π of A as a subset π * of A * .

The category of sets and relations

It is the category \mathbf{Rel} whose objects are sets, and such that \mathbf{Rel}(X,Y)=\mathcal P(X\times Y). Composition is the ordinary composition of relations: given s\in\mathbf{Rel}(X,Y) and t\in\mathbf{Rel}(Y,Z), one sets

t\circ s=\set{(a,c)\in X\times Z}{\exists b\in Y\ (a,b)\in s\ \text{and}\ (b,c)\in t}.

Personal tools