Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

DOI10.2168/LMCS-2(2:1)2006MaRDI QIDQ5310654zbMATH OpenFDO

Authors Kristian Støvring

Publication date 11 October 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/math/0602544

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Abstract: We answer Klop and de Vrijer's question whether adding surjective-pairing axioms to the extensional lambda calculus yields a conservative extension. The answer is positive. As a byproduct we obtain a "syntactic" proof that the extensional lambda calculus with surjective pairing is consistent.

Recommendations

• scientific article; zbMATH DE number 4179332
• Unique normal forms for lambda calculus with surjective pairing
• scientific article; zbMATH DE number 176742
• scientific article; zbMATH DE number 2053247
• A confluent reduction for the λ-calculus with surjective pairing and terminal object

Cited in

(12)

• Unique normal forms for lambda calculus with surjective pairing
• How to think of intersection types as Cartesian products
• Functional pearl: the distributive \(\lambda\)-calculus
• On polymorphic types of untyped terms
• Certifying confluence proofs via relative termination and rule labeling
• Cartesian monoids
• scientific article; zbMATH DE number 4179332 (Why is no real title available?)
• Pairings on Lambda Algebras
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• scientific article; zbMATH DE number 7204433 (Why is no real title available?)
• Extensional proofs in a propositional logic modulo isomorphisms
• Title not available (Why is no real title available?)

Describes a project that uses

Uses Software

• Twelf

This page was built for publication: Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5310654)