Mariangiola Dezani, Robert Meyer, and Yoko Motohama
The semantics of entailment omega
Notre Dame J. Formal Logic, 43(3):129-145, 2002
This paper discusses the relation between the minimal positive relevant
logic B+ and intersection and union type theories. There is a
marvellous coincidence between these very differently motivated research
areas. First, we show a perfect fit between the Intersection Type
Discipline ITD and the tweaking B/\ T of B+,
which saves implication -> and conjunction /\ but drops
disjunction V. The filter models of the
lambda-calculus (and its intimate partner Combinatory Logic
CL) of the first author and her co-authors then become theory
models of these calculi. (The logician's Theory is the algebraist's
Filter.) The coincidence extends to a dual interpretation of key
particles - the subtype <= translates to provable ->, type intersection to conjunction
/\, function space -> to implication and whole domain omega
to the (trivially added but trivial) truth T. This satisfying
ointment contains a fly. For it is right, proper and to be expected
that type union U should correspond to the logical disjunction
V of B+. But the simulation of functional application by a
fusion (or modus ponens product) operation o on theories leaves
the key Bubbling lemma of work on ITD unprovable for the
V-prime theories now appropriate for the modelling. The focus
of the present paper lies in an appeal to Harrop theories which
are (a) prime and (b) closed under fusion. A version of the Bubbling
lemma is then proved for Harrop theories, which accordingly furnish a
model of lambda and CL.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43