Home » forums » LtU Forum

A simple class of Kripke-style models in which logic and computation have equal standing

A simple class of Kripke-style models in which logic and computation have equal standing, Michael and Murdoch Gabbay, LPAR 2010:

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.

By dpmulligan at 2010-07-13 09:33 | LtU Forum | previous forum topic | next forum topic | other blogs | 5292 reads

Comment viewing options

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

affinity with Curry Howard ?

Glimpsing over it (although I should pursue other endeavours) it sounds pretty interesting.

The affinity with Curry Howard type of results is striking. Nevertheless the authors shy away from calling it that. Do you know something more?

By Spyros Komninos at Wed, 2010-07-14 17:48 | login or register to post comments

Curry-Howard Correspondence

Curry-Howard is: Types --- Formulae, Programs --- Proofs.

In this work, we have lambda terms as formulae, not as proofs, so we get a mixed metaphor.

One might try to look at the proof system and try to expose a programming language, but it's Hilbert-style, which complicates things.

What puzzles me the most, though, is what can be the use of such a logic.

By Ohad Kammar at Thu, 2010-07-22 09:59 | login or register to post comments

Proof theory for untyped lambda calculus

There is an interesting sequent logic, satisfying cut-elimination, associated with these models. It is described in a forthcoming JSL paper:

A proof theoretic treatment of lambda-reduction with cut-elimination: lambda-calculus as a logic programming language

The sequent logic of that paper is just for the familiar language of lambda terms, and not for the full lambda-terms-as-formulae logic (although it can be extended).

We have not determined what term language corresponds to derivations in this sequent system, it is certainly an interesting question.

By Gabbay at Sat, 2010-07-24 15:34 | login or register to post comments