We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
CONVERSE EXTENSIONALITY AND APARTNESS.
- Authors
VAN DEN BERG, BENNO; PASSMANN, ROBERT
- Abstract
In this paper we try to find a computational interpretation for a strong form of extensionality, which we call "converse extensionality". Converse extensionality principles, which arise as the Dialectica interpretation of the axiom of extensionality, were first studied by Howard. In order to give a computational interpretation to these principles, we reconsider Brouwer's apartness relation, a strong constructive form of inequality. Formally, we provide a categorical construction to endow every typed combinatory algebra with an apartness relation. We then exploit that functions reect apartness, in addition to preserving equality, to prove that the resulting categories of assemblies model a converse extensionality principle.
- Subjects
RELATION algebras; PROOF theory; AXIOMS
- Publication
Logical Methods in Computer Science (LMCS), 2022, Vol 18, Issue 4, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.46298/LMCS-18(4:13)2022