What is meant by a full abstract model of a lambda-calculus like language?

The simply typed lambda-calculus with numbers and fix has long been a favorite experimental subject for programming language researchers, since it is the simplest language in which a range of subtle semantic phenomena such as full abstraction arise.

I tried to find a definition for full-abstract model but I haven't found such. This quote is from Pierce's TAPL book. Note that there is also a related question: What is a "model" of lambda calculus? on the site that has not been answered.

• Full abstraction is used in when you are working in denotational semantics for a programming language. A model is fully abstract when semantic equivalence implies contextual equivalence. I think it was introduced by Milner sciencedirect.com/science/article/pii/0304397577900536 Nov 7, 2019 at 15:52
• the answer to this can be found in a series of lectures in Winter School on Denotational Semantics (30 Jan - 3 Feb, 2017) Mar 25, 2020 at 14:41

In denotational semantics, you want to be able to map each of your language terms to some object in your semantic domain or model. Now, it cannot be any arbitrary domain/model as you like, but, informally speaking, something that gives a good intuition about how the language works (its computational behavior).

Milner tried to formalize what this "intuition" should be and called it full abstraction. Formally, a model is fully abstract if all observationally equivalent terms in the object language represent the same object in the model. Equationally: $$\text{if } ⟦t_1⟧ = ⟦t_2⟧ \text{then } t_1 \rightsquigarrow t_2$$ where $$\rightsquigarrow$$ represents observational equivalence. In case of lambda-calculus observational equivalence would be $$\beta\eta\alpha$$ conversions and $$⟦\_⟧$$ is the denotation function.

There are few papers that you might want to take a look at if you are interested in seeing some full abstract models of lambda like languages:

1. Plotkin's paper that gives a full abstract model of the lambda like language called LCF
2. Mulmuley's paper gives a full abstract model of typed lambda calculus.
3. Hyland and Ong's papers give a full abstract model of PCF using game semantics
• Surely the equation you wrote is simply the soundness of the model, full abstraction should go in the other direction no?
– cody
Nov 9, 2019 at 19:52
• @cody indeed. fixed it now. Nov 11, 2019 at 17:16