Abstract
We present two results which relate dinaturality with a syntactic property (typability) and a semantic one (interpretability by betaetastable sets). First, we prove that closed dinatural lambdaterms are simply typable, that is, the converse of the wellknown fact that simply typable closed terms are dinatural. The argument exposes a syntactical aspect of dinaturality, as lambdaterms are typechecked by computing their associated dinaturality equation. Second, we prove that a closed lambdaterm belonging to all betaetastable 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 betaetastable semantics with respect to simple types. While the completeness of this semantics is wellknown 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 betaetaStable Models}},
booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
pages = {29:129:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770477},
ISSN = {18688969},
year = {2017},
volume = {84},
editor = {Dale Miller},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7729},
URN = {urn:nbn:de:0030drops77291},
doi = {10.4230/LIPIcs.FSCD.2017.29},
annote = {Keywords: Dinaturality, simplytyped lambdacalculus, betaetastable semantics, completeness}
}
Keywords: 

Dinaturality, simplytyped lambdacalculus, betaetastable semantics, completeness 
Collection: 

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) 
Issue Date: 

2017 
Date of publication: 

30.08.2017 