<p>Full abstraction means that denotational equality coincides with observational equivalence (under all contexts), but that notion depends on what observations you choose. If your observation on a term is whether it admits a head-normal form, then the associated observational equivalence is called <span class="math-container">$\mathcal{H}^*$</span> and many fully abstract models are known for it, including Scott's original domain-theoretic model. See this paper by Flavien Breuvart for more: <a href="https://lmcs.episciences.org/1636" rel="nofollow noreferrer">https://lmcs.episciences.org/1636</a></p>

CC BY-SA 4.0
2024-03-06T22:43:25.473Z
2024-03-06T22:43:25.473Z
Lê Thành Dũng 'Tito' Nguyễn
<p>Famously, the denotational semantics of PCF in Scott domains is not fully abstract. But by adding the parallel or construct to PCF, a fully abstract semantics can be obtained.</p>
<p>Is there an analogous result for the untyped lambda calculus? Is the Scott semantics for the untyped lambda calculus with parallel or known to be fully abstract? If not, is there a similar feature that can be added to obtain a fully abstract semantics?</p>

<lambda-calculus><denotational-semantics>
Is there a full abstraction result for an untyped lambda calculus?
Nick Rioux
# Is there a full abstraction result for an untyped lambda calculus?

(Asked by: username_0 on 2024-03-06)

Famously, the denotational semantics of PCF in Scott domains is not fully abstract. But by adding the parallel or construct to PCF, a fully abstract semantics can be obtained.

Is there an analogous result for the untyped lambda calculus? Is the Scott semantics for the untyped lambda calculus with parallel or known to be fully abstract? If not, is there a similar feature that can be added to obtain a fully abstract semantics?

**Tags:** lambda-calculus, denotational-semantics


---

## 1 answers

### Answer by username_1 on 2024-03-06. Score: 4

Full abstraction means that denotational equality coincides with observational equivalence (under all contexts), but that notion depends on what observations you choose. If your observation on a term is whether it admits a head-normal form, then the associated observational equivalence is called $\mathcal{H}^\*$ and many fully abstract models are known for it, including Scott's original domain-theoretic model. See this paper by Flavien Breuvart for more: <https://lmcs.episciences.org/1636>


---

