Hostname: page-component-745bb68f8f-grxwn Total loading time: 0 Render date: 2025-02-11T05:36:57.789Z Has data issue: false hasContentIssue false
  • English
  • Français

Conditions for the completeness of functional and algebraic equational reasoning

Published online by Cambridge University Press:  01 December 1999

JON G. RIECKE  and
RAMESH SUBRAHMANYAM
JON G. RIECKE
Affiliation:
Bell Laboratories, Lucent Technologies, 700 Mountain Avenue, Murray Hill, New Jersey 07974, USA
RAMESH SUBRAHMANYAM
Affiliation:
Department of Mathematics, Wesleyan University, Middletown, Connecticut 06459, USA Current address: Lucent Technologies, 2000 Naperville Road, PO Box 3033, Naperville, Illinois 60566-7033, USA.
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We consider the following question: in the simply-typed λ-calculus with algebraic operations, is the set of equations valid in a particular model exactly those provable from (β), (η) and the set of algebraic equations, E, that are valid in the model? We find conditions for determining whether βηE-equational reasoning is complete. We demonstrate the utility of the results by presenting a number of simple corollaries for particular models.

Type
Research Article
Information
Mathematical Structures in Computer Science , Volume 9 , Issue 6 , December 1999 , pp. 651 - 685
Copyright
1999 Cambridge University Press

Footnotes

A preliminary version titled ‘Algebraic Reasoning and Completeness in Typed Languages’ appeared in Twentieth ACM Conference on Principles of Programming Languages, pages 185–195, ACM Press, 1993.