Skip to content

Abstracts.2020.LogicalRel

Jump to bottom
Fabian edited this page May 6, 2021 · 4 revisions

Logical Relations

by Andreas Abel

Abstract

We start Model May with a lecture on logical relations. I will present logical relations for

  • simply-typed combinatory logic (variable-free λ-calculus)
  • simply-typed λ-calculus (STLC)

Material

Notes

Let 𝒞 be a locally small category with a terminal object 𝟏.

The global sections functor Γ is defined as the functor Hom ( 𝟏 , – ) : 𝒞 → Set that sends objects X to the set Hom ( 𝟏 , X ) .

Γ preserves (small) limits.[nLab]

The scone or Freyd cover 𝒞 ¯ is defined as the category Set ↓ Γ whose objects are given by a set M, an object X and a function f : M → Γ ( X ) .

If 𝒞 is cartesian closed, then so are 𝒞 ¯ and 𝒞 ¯ → 𝒞 . This holds more generally for 𝒟 ↓ F → 𝒟 when the category 𝒟 is finitely complete and cartesian closed, and the functor F : 𝒞 → 𝒟 preserves finite products.

References

  1. G.D. Plotkin. Lambda-definability and logical relations. Memorandum, School of Artificial Intelligence, University of Edinburgh, 1973.
  2. G.D. Plotkin. Lambda-definability in the full type hierarchy. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 363–373. Academic Press, 1980.
  3. H. Friedman. Equality between Functionals. In R. Parikh, editor, Logic Colloquium — Symposium on Logic held at Boston 1972–73, Lecture Notes in Mathematics, volume 453, pages 22–37. Berlin, Heidelberg, 1975.

Bibliography

  1. J.C. Mitchell and A. Scedrov. Notes on sconing and relators. In CSL’92, pages 352–378. Springer Verlag LNCS 702, 1993.

  2. M. Shulman. Scones, Logical Relations, and Parametricity. On The n-Category Café, 2013.

  3. R.O. Gandy. On Axiomatic Systems in Mathematics and Theories in Physics. University of Cambridge, UK, 1953.

  4. W.A. Howard. Hereditarily Majorizable Functionals of Finite Type. In A.S. Troelstra, editor, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, pages 454–485. Berlin, Heidelberg, 1973.

  5. Robert Milne. The Formal Semantics of Computer Languages and their Implementations. University of Cambridge, UK, 1974.

  6. J.C. Reynolds. Types, Abstraction and Parametric Polymorphism. International Federation for Information Processing Congress 1983, pages 513–523, 1983.

  7. C. Hermida, U.S. Reddy, and E.P. Robinson. Logical Relations and Parametricity — A Reynolds Programme for Category Theory and Programming Languages. Electronic Notes in Theoretical Computer Science, Volume 303, pages 149–180, 2014.

  8. P.J. Freyd and A. Scedrov. Categories, Allegories. Mathematical Library, North-Holland, 1990.

  9. J. Lambek and P.J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge studies in advanced mathematics 7, Cambridge University Press, 1986.

  10. A. Scedrov and P.J. Scott. A note on the Friedman slash and Freyd covers. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Symposium, pages 443–452. North-Holland, 1982.

  11. Y. Lafont. Logiques, Categories & Machines. Thèse de Doctorat, Université Paris VII, 1988.

  12. R. Statman. Logical relations and the typed lambda calculus. Information and Control, 65:85–97, 1985.

  13. J.C. Mitchell. Type systems for programming languages. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 365–458. North-Holland, 1990.

Related Talks

Clone this wiki locally