Extending PowerEpsilon with algebraic rewriting
Li-Xin Zeng, Ming-Yuan Zhu · ACM SIGPLAN Notices · 1994
PowerEpsilon ([ZhuW9l]) is a strongly-typed polymorphic functional programming language based on Martin-Löf's type theory and the Calculus of Constructions. In PowerEpsilon there are no constant time definitions of the predecessor functions which will lead to non-efficient programs. In this paper, we give a solution to this problem by introducing an algebraic rewriting mechanism into the system.