License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.29
URN: urn:nbn:de:0030-drops-77291
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7729/
Go to the corresponding LIPIcs Volume Portal

Pistone, Paolo

On Dinaturality, Typability and beta-eta-Stable Models

pdf-format:
LIPIcs-FSCD-2017-29.pdf (0.5 MB)

Abstract

We present two results which relate dinaturality with a syntactic property (typability) and a semantic one (interpretability by beta-eta-stable sets). First, we prove that closed dinatural lambda-terms are simply typable, that is, the converse of the well-known fact that simply typable closed terms are dinatural. The argument exposes a syntactical aspect of dinaturality, as lambda-terms are type-checked by computing their associated dinaturality equation. Second, we prove that a closed lambda-term belonging to all beta-eta-stable interpretations of a simple type must be dinatural, that is, we prove dinaturality by semantical means. To do this, we show that such terms satisfy a suitable version of binary parametricity and we derive dinaturality from it.

By combining the two results we obtain a new proof of the completeness of beta-eta-stable semantics with respect to simple types. While the completeness of this semantics is well-known in the literature, the technique here developed suggests that dinaturality might be exploited to prove completeness also for other, less manageable, semantics (like saturated families or reducibility candidates) for which a direct argument is not yet known.

BibTeX - Entry

@InProceedings{pistone:LIPIcs:2017:7729,
  author =	{Paolo Pistone},
  title =	{{On Dinaturality, Typability and beta-eta-Stable Models}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7729},
  URN =		{urn:nbn:de:0030-drops-77291},
  doi =		{10.4230/LIPIcs.FSCD.2017.29},
  annote =	{Keywords: Dinaturality, simply-typed lambda-calculus, beta-eta-stable semantics, completeness}
}

Keywords: Dinaturality, simply-typed lambda-calculus, beta-eta-stable semantics, completeness
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI