A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus

1976/02/01 by Martin Hyland · 1 voice · 2 citations
Computer Science · Economics, Econometrics and Finance · #Advanced Algebra and Logic #Game Theory and Voting Systems #semigroups and automata theory

paper · doi:10.1112/jlms/s2-12.3.361

openalex publication_date 1976/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/04/16

Abstract

An equality relation on the terms of the A-calculus is an equivalence relation closed under the (syntactical) operations of application and A-abstraction. We may distinguish between syntactic and semantic ways of introducing equality relations, /^-equality is introduced syntactically; it is the least equality relation satisfying the

Cited by

• Dynamic Backward Slicing of Rewriting Logic Computations
• On the characterization of models of H* : The operational aspect

Discussions

• [61] = M. Hyland, “A syntactic characterization of the equality in some models […]”, ‘J. London Math. Soc.’ 12 (2) (1976) 361–370 doi.org/10.1112/jlms... [86] = G. Longo, “Set-theoretical models of λ [bsky, 1 points, 0 comments]

Related

• Making Logical Relations More Relatable (Proof Pearl)
• Semantic Analysis of Normalisation by Evaluation for Typed Lambda Calculus
• Lambda Calculus Synopsis
• Case Studies in Formal Reasoning About Lambda-Calculus: Semantics, Church-Rosser, Standardization and HOAS
• Lambda Congruences and Extensionality