A Simple and Complete Model Theory for Intensional and Extensional Untyped Lambda-Equality
Authors
Gabbay, MJ
Gabbay, Murdoch
Change log
Abstract
We present a sound and complete model theory for theories of -reduction with or without -expansion. The models of this paper derive from structures of modal logic: we use ternary accessibility relations on ‘possible worlds’ to model the action of intensional and extensional lambda-abstraction in much the same way binary accessibility relations are used to model the box operators of a normal multi-modal logic.
Publication Date
2014-12-24
Online Publication Date
2014-12-12
Acceptance Date
2014-08-31
Keywords
Journal Title
IfCoLoG Journal of Logics and their Applications
Journal ISSN
Volume Title
1
Publisher
College Publications
Sponsorship
International Federation for Computational Logic (IFCoLog) (unknown)