[TYPES] models of untyped lambda calculus

[Gabriel Scherer]

The paper that Albert referred to is

 What is a model of the lambda calculus?
 Albert Meyer, 1982


> An elementary, purely algebraic definition of model for the untyped lambda
> calculus is given. This definition is shown to be equivalent to the natural
> semantic definition based on environments. These definitions of model are
> consistent with, and yield a completeness theorem for, the standard axioms
> for lambda convertibility. A simple construction of models for lambda
> calculus is reviewed. The algebraic formulation clarifies the relation
> between combinators and lambda terms.


  https://www.sciencedirect.com/science/article/pii/S0019995882800879

The fact that the only practical way to access a PDF of this work is from
ScienceDirect (the version attached by Albert also comes from this website)
should serve as a reminder to everyone to upload their paper on arXiv for
proper open access and long-term archival:
  https://arxiv.org/ .
You may thank yourself 36 years from now.

On Sat, Sep 22, 2018 at 3:35 PM Artem Pelenitsyn <a.pelenitsyn at gmail.com>
wrote:

> Dear Albert,
>
> I don't see anything attached to your mail, unfortunately.
>
> --
> Best wishes,
> Artem Pelenitsyn
>
> On Fri, Sep 21, 2018, 2:22 PM Albert R Meyer <ameyer at mit.edu> wrote:
>
>> [ The Types Forum,
>> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>>
>> 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
>> > >
>> >
>>
>