Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/158511.158627acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
Article
Free access

Algebraic reasoning and completeness in typed languages

Published: 01 March 1993 Publication History

Abstract

We consider the following problem in proving observational congruences in functional languages: given a call-by-name language based on the simply-typed λ-calculus with algebraic operations axiomatized by algebraic equations E, is the set of observational congruences between terms exactly those provable from (β), (η), and E? We find conditions for determining whether βηE-equational reasoning is complete for proving the observational congruences between such terms. We demonstrate the power and generality of the theorems by presenting a number of easy corollaries for particular algebras.

References

[1]
Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison- Wesley, 1990.
[2]
Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic. North-Holland, 1981. Revised Edition, 1984.
[3]
Val Breazu-Tannen. Combining algebra and higher-order types. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 82-90. IEEE, 1988.
[4]
Stavros S. Cosmadakis. Computing with recursive types. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 24-38. IEEE, 1989.
[5]
Harvey Friedman. Equality between functionals. In Rohit Parikh, editor, Logic Colloquium '73, volume 453 of Lect. Notes in Math., pages 22-37. Springer-Verlag, 1975.
[6]
Albert 1%. Meyer. What is a model of the lambda calculus? Information and Control, 52:87-122, 1982.
[7]
Robin Milner. Fully abstract models of the typed lambda calculus. Theoretical Computer Sci., 4:1- 22, 1977.
[8]
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: A Formal Introduction. John Wiley & Sons, 1992.
[9]
Tobias Nipkow and Zhenyu Qian. Modular higherorder E-unification. In Ronald V. Book, editor, Rewriting Techniques and Applications, volume 488 of Lect. Notes in Computer Sci., pages 200- 214. Springer-Verlag, 1991.
[10]
Chih-Hao Luke Ong. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. PhD thesis, Imperial College, University of London, 1988.
[11]
Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223- 257, 1977.
[12]
Jon G. Riecke. The Logic and Expressibility of Simply-Typed Call-by-Value and Lazy Languages. PhD thesis, Massachusetts Institute of Technology, 1991. Available as technical report MIT/LCS/TR-523 (MIT Laboratory for Computer Science).
[13]
Jon G. Riecke. Statman's 1-section theorem. Technical Report MS-CIS-92-03, University of Pennsylvania, Department of Computer and Information Science, January 1992. Submitted for publication to Information and Computation.
[14]
V.Yu. Sazonov. Expressibility of functions in D. Scott's LCF language. Algebra i Logika, 15:308- 330, 1976. Russian.
[15]
Dana Scott. A type theoretical alternative to CUCH, ISWIM, OWHY. Unpublished manuscript, Oxford University, 1969.
[16]
Richard Statman. Completeness, invariance and lambda-definability. J. Symbolic Logic, 47:17-26, 1982.
[17]
Richard Statman. Equality between functionals revisited. In L.A. Harrington, et al., editor, Harvey Friedman's Research on the Foundations of Mathematics, volume 117 of Studies in Logic, pages 331-338. North-Holland, 1985.

Cited By

View all
  • (2005)SPCF: its model, calculus, and computational powerSemantics: Foundations and Applications10.1007/3-540-56596-5_39(318-347)Online publication date: 3-Jun-2005

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '93: Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
March 1993
510 pages
ISBN:0897915607
DOI:10.1145/158511
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 March 1993

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

POPL93

Acceptance Rates

POPL '93 Paper Acceptance Rate 39 of 199 submissions, 20%;
Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)27
  • Downloads (Last 6 weeks)9
Reflects downloads up to 14 Nov 2024

Other Metrics

Citations

Cited By

View all
  • (2005)SPCF: its model, calculus, and computational powerSemantics: Foundations and Applications10.1007/3-540-56596-5_39(318-347)Online publication date: 3-Jun-2005

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Get Access

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media