Conditions for the completeness of functional and algebraic equational reasoningA 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.
RIECKE, JON G.; SUBRAHMANYAM, RAMESH; RIECKE JON G.; Bell Laboratories, Lucent Technologies; SUBRAHMANYAM RAMESH; Wesleyan University; Lucent Technologies
Журнал:
Mathematical Structures in Computer Science
Дата:
1999
Аннотация:
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.
415.1Кб