2018/01/16 by Flavien Breuvart, Breuvart, Flavien
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1801.05150
openalex created_date 2016/06/24 · openalex publication_date 2018/01/16 · openalex updated_date 2026/07/28
We give a characterization, with respect to a large class of models of untyped λ-calculus, of those models that are fully abstract for head-normalization, i.e., whose equational theory is H^*. An extensional K-model D is fully abstract if and only if it is hyperimmune, i.e., non-well founded chains of elements of D cannot be captured by any recursive function. This article share its first title with its companion paper and a short version. It is a standalone paper that present a purely syntactical proof of the result as opposed to its companion paper that present an independent and purely semantical proof of the exact same result.