On Dinaturality, Typability and beta-eta-Stable Models

Author Paolo Pistone



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2017.29.pdf
  • Filesize: 0.51 MB
  • 17 pages

Document Identifiers

Author Details

Paolo Pistone

Cite As Get BibTex

Paolo Pistone. On Dinaturality, Typability and beta-eta-Stable Models. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.29

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.

Subject Classification

Keywords
  • Dinaturality
  • simply-typed lambda-calculus
  • beta-eta-stable semantics
  • completeness

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. E. S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35-64, 1990. Google Scholar
  2. Joachim de Lataillade. Dinatural terms in System F. In Proceedings of the Twenty-Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009), pages 267-276, Los Angeles, California, USA, 2009. IEEE Computer Society Press. Google Scholar
  3. Samir Farkh and Karim Nour. Résultats de complétude pour des classes de types du système AF2. Informatique Théorique et Applications, 31(6):513-537, 1998. Google Scholar
  4. Jean Gallier. On Girard’s "candidats de réductibilité". Logic and Computer Science, 1990. Google Scholar
  5. Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Normal forms and cut-free proofs as natural transformations. In Y. Moschovakis, editor, Logic from Computer Science, volume 21, pages 217-241. Springer-Verlag, 1992. Google Scholar
  6. Roger J. Hindley. The completeness theorem for typing λ-terms. Theoretical Computer Science, 22(1-2):1-17, 1983. Google Scholar
  7. Jean-Louis Krivine. Lambda calculus, types and models. Ellis Horwood, 1993. Google Scholar
  8. R. Labib-Sami. Types avec (ou sans) types auxiliaires. Manuscript, 1986. Google Scholar
  9. Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In TLCA'93, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361-375. Springer Berlin Heidelberg, 1993. Google Scholar
  10. John C. Reynolds. Types, abstraction and parametric polymorphism. In R.E.A. Mason, editor, Information Processing 1983, pages 513-523. North-Holland, 1983. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail