Re: [TYPES] models of untyped lambda calculus

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

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-0AtTguNXcGkudfPDI7pAfjevRRvlBcP1@public.gmane.org] on behalf of Rosu, Grigore [grosu-nzINlOoChub2fBVCVOL8/[email protected]]
Sent: Sunday, September 16, 2018 5:29 PM
To: types-list-nHFbR+4dATOoZA3Q9b/[email protected]
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,
Grigore