[TYPES] models of untyped lambda calculus

[Albert R Meyer]

perhaps my old paper, attached, is relevant here.
Yours truly,

Albert R. Meyer
Professor of Computer Science
MIT Department of Electrical Engineering and Computer Science
Cambridge MA 02139


On Fri, Sep 21, 2018 at 3:04 AM Gabriel Scherer <gabriel.scherer at gmail.com>
wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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
> >
>