[TYPES] models of untyped lambda calculus

Rosu, Grigore grosu at illinois.edu
Thu Sep 20 20:22:20 EDT 2018

Still looking for an answer to this question.  Thank you, Mariangiola Dezani, for referring us to open problem #22 in the TLCA list: http://tlca.di.unito.it/opltlca/.  That was indeed what we initially had in mind, continuously complete CPOs.  But now, seeing that the problem is still open, we are willing to weaken our requirements as much as possible provided the resulting structures can still be reasonably called "conventional models".  Specifically, we want to avoid models which come with given interpretations of all the terms (satisfying constraints).  Instead, we want models where the interpretation of `lambda x . e` under `rho` can be constructed from the interpretations of `e` under `rho[m/x]` for all appropriate `m` in `M`.

Thank you,
Grigore and Xiaohong

From: Types-list [types-list-bounces at LISTS.SEAS.UPENN.EDU] on behalf of Rosu, Grigore [grosu at illinois.edu]
Sent: Sunday, September 16, 2018 5:29 PM
To: types-list at lists.seas.upenn.edu
Subject: [TYPES] models of untyped lambda calculus

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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.

Thank you,

More information about the Types-list mailing list