Hostname: page-component-74656f9884-npj9w Total loading time: 0 Render date: 2026-11-07T12:12:26.199Z Has data issue: false hasContentIssue false

Normalization and the Yoneda embedding

Published online by Cambridge University Press:  01 April 1998

DJORDJE ČUBRIĆ
Affiliation:
DPMMS, University of Cambridge, 16 Mill Lane, Cambridge CB2 1SB, UK. Email: cubric@triples.math.mcgill.ca
PETER DYBJER
Affiliation:
Department of Computing Science, Chalmers University of Technology, S-412 96 Göteborg, Sweden. Email: peterd@cs.chalmers.se
PHILIP SCOTT
Affiliation:
Department of Mathematics, University of Ottawa, 585 King Edward, Ottawa, Ontario K1N 6N5, Canada. Email: phil@mathstat.uottawa.ca
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.

Information

Type
Research Article
Copyright
1998 Cambridge University Press