DocumentCode
3294400
Title
Equality between functionals in the presence of coproducts
Author
Dougherty, Daniel J. ; Subrahmanyam, Ramesh
Author_Institution
Dept. of Math., Wesleyan Univ., Middletown, CT, USA
fYear
1995
fDate
26-29 Jun 1995
Firstpage
282
Lastpage
291
Abstract
Consider the simply-typed lambda calculus with sum-type constructors, and let Set be the standard set-theoretic model of this calculus over an infinite base set. We present a proof system for the calculus (which involves a rule for reasoning by cases) and prove it to be a complete axiomatization of the equational theory of Set. We also develop some results concerning the syntactic properties of the calculus and an interpretation in Set of the equational theory (in the language of the classical simply-typed calculus) of the full function hierarchy over one infinite and one finite base set
Keywords
functional analysis; functional equations; lambda calculus; coproducts; full function hierarchy; functional; infinite base set; proof system; simply-typed lambda calculus; standard set-theoretic model; sum-type constructors; Calculus; Encoding; Equations; Helium;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location
San Diego, CA
ISSN
1043-6871
Print_ISBN
0-8186-7050-9
Type
conf
DOI
10.1109/LICS.1995.523263
Filename
523263
Link To Document