[TYPES] models of untyped lambda calculus
grosu at illinois.edu
Sun Sep 16 18:29:39 EDT 2018
Are there conventional models of untyped lambda calculus for which equational deduction with alpha+beta is *complete*? By conventional models I mean ones where lambda and application are interpreted as functions.
The Hindley-Longo style models are complete but non-conventional. On the other hand, graph models are conventional but incomplete.
More information about the Types-list