[TYPES] models of untyped lambda calculus

[Gabriel Scherer]

Dear Grigore and Xiaohong,

It may be helpful to make the question a bit more self-contained -- or
even if we cannot help answer, some of us on the list would at last
learn from the question.
- I am not sure what "complete" means in your question, recalling the
definition would help.
- I am not familiar with the Hindley-Longo and graph models that you
refer to, do you have some pointers to introductory presentations?

(Intuitively I would expect models mapping lambda-terms to
mathematical functions to respect "eta" (for the function type), and
thus have stronger identifications than just alpha+beta.)
On Fri, Sep 21, 2018 at 7:04 AM Rosu, Grigore <grosu at illinois.edu> wrote:
>
> [ 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 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,
> Grigore
>