Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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:
