# 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 – Apoorv Nov 7 '19 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) – Rodrigo Mar 25 '20 at 14:41

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.