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.

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:

• Plotkin's paper that gives a full abstract model of the lambda like language called LCF

• Mulmuley's paper gives a full abstract model of typed lambda calculus.

• Hyland and Ong's papers give a full abstract model of PCF using game semantics

StackExchange Computer Science Q#116807, answer score: 8