6
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ 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 $\endgroup$ – Apoorv Nov 7 '19 at 15:52
  • $\begingroup$ the answer to this can be found in a series of lectures in Winter School on Denotational Semantics (30 Jan - 3 Feb, 2017) $\endgroup$ – Rodrigo Mar 25 '20 at 14:41
6
$\begingroup$

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
Improve this answer
$\endgroup$
2
  • $\begingroup$ Surely the equation you wrote is simply the soundness of the model, full abstraction should go in the other direction no? $\endgroup$ – cody Nov 9 '19 at 19:52
  • 1
    $\begingroup$ @cody indeed. fixed it now. $\endgroup$ – Apoorv Nov 11 '19 at 17:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.