Sciweavers

Share
LPAR
2010
Springer

A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing

3 years 6 months ago
A Simple Class of Kripke-Style Models in Which Logic and Computation Have Equal Standing
We present a sound and complete model of lambda-calculus reductions based on structures inspired by modal logic (closely related to Kripke structures). Accordingly we can construct a logic which is sound and complete for the same models, and we identify lambda-terms with certain simple sentences (predicates) in this logic, by direct compositional translation. Reduction then becomes identified with logical entailment. Thus, the models suggest a new way to identify logic and computation. Both have elementary and concrete representations in our models; where these representations overlap, they coincide. In a concluding speculation, we note a certain subclass of the models which seems to play a role analogous to that played by the cumulative hierarchy models in axiomatic set theory and the natural numbers in formal arithmetic -- there are many models of the respective theories, but only some, characterised by a fully second order interpretation, are the `intended' ones.
Michael Gabbay, Murdoch James Gabbay
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Michael Gabbay, Murdoch James Gabbay
Comments (0)
books