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

lmcs:3235 - Logical Methods in Computer Science, July 20, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:2)2018
Relational Graph Models at WorkArticle

Authors: Flavien Breuvart ; Giulio Manzonetto ; Domenico Ruoppolo

    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
    Accepted on: June 27, 2018
    Submitted on: March 31, 2017
    Keywords: Computer Science - Logic in Computer Science

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1565 times.
    This article's PDF has been downloaded 440 times.