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

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

Authors: Flavien Breuvart 

Publication date: 28 April 2016

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

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.

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

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

zbMATH Keywords

full abstractiondomainslambda calculusobservational equivalence

Mathematics Subject Classification ID

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

Cited In (3)

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

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)