Breuvart, Flavien and Manzonetto, Giulio and Ruoppolo, Domenico - Relational Graph Models at Work

lmcs:3235 - Logical Methods in Computer Science, July 20, 2018, Volume 14, Issue 3 -
Relational Graph Models at Work

Authors: Breuvart, Flavien and Manzonetto, Giulio and Ruoppolo, Domenico

We study the relational graph models that constitute a natural subclass of relational models of lambda-calculus. We prove that among the lambda-theories induced by such models there exists a minimal one, and that the corresponding relational graph model is very natural and easy to construct. We then study relational graph models that are fully abstract, in the sense that they capture some observational equivalence between lambda-terms. We focus on the two main observational equivalences in the lambda-calculus, the theory H+ generated by taking as observables the beta-normal forms, and H* generated by considering as observables the head normal forms. On the one hand we introduce a notion of lambda-König model and prove that a relational graph model is fully abstract for H+ if and only if it is extensional and lambda-König. On the other hand we show that the dual notion of hyperimmune model, together with extensionality, captures the full abstraction for H*.

Volume: Volume 14, Issue 3
Published on: July 20, 2018
Submitted on: March 31, 2017
Keywords: Computer Science - Logic in Computer Science


Consultation statistics

This page has been seen 321 times.
This article's PDF has been downloaded 250 times.