On the characterization of models of H^: the semantical aspect

DOI10.2168/LMCS-12(2:4)2016zbMATH Open1338.03013OpenAlexW3102779848MaRDI QIDQ2804203FDOQ2804203

Authors Flavien Breuvart 

Publication date 28 April 2016

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.07259

zbMATH Keywords

full abstractiondomainslambda calculusobservational equivalence

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Abstract: We give a characterization, with respect to a large class of models of untyped lambda-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H* (observations for head normalization). An extensional K-model $D$ is fully abstract if and only if it is hyperimmune, {em i.e.}, not well founded chains of elements of D cannot be captured by any recursive function. This article, together with its companion paper, form the long version of [Bre14]. It is a standalone paper that presents a purely semantical proof of the result as opposed to its companion paper that presents an independent and purely syntactical proof of the same result.

Recommendations

• On the characterization of models of \(\mathcal{H}^*\)
• Relational graph models at work
• Full abstraction in the lazy lambda calculus
• Lambda Theories of Effective Lambda Models
• scientific article; zbMATH DE number 883584

Cited in

(3)

• On the characterization of models of \(\mathcal{H}^*\)
• Behavioural inverse limit \(\lambda\)-models
• Relational graph models at work

This page was built for publication: On the characterization of models of \(\mathcal H^\ast\): the semantical aspect

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2804203)