![Cover Image for System.Linq.Enumerable+EnumerablePartition`1[System.Char]](https://coverimages.igi-global.com/images/search-article.png)
A Simple and Complete Model Theory for Intensional and Extensional Untyped Lambda-Equality
OAI: oai:www.repository.cam.ac.uk:1810/295072 • DOI: 10.17863/CAM.42150
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.