[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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 <[email protected]> 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 < >> [email protected]> >> 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 <[email protected]> >> 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 [[email protected]] on behalf >> of >> > Rosu, Grigore [[email protected]] >> > > Sent: Sunday, September 16, 2018 5:29 PM >> > > To: [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 >> > > >> > >> >
