Rewriting Calculus with Fixpoints: Untyped and First-Order Systems
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems
复制标题
用不动点重写微积分：无类型和一阶系统
DOI：
10.1007/978-3-540-24849-1_10
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Benjamin Wack
中科院分区：
文献类型：
--
作者：
Horatiu Cirstea;L. Liquori;Benjamin Wack
重写演算，也称为ρ演算，是一个嵌入λ演算和重写能力的框架，不仅允许对变量进行抽象，而且允许对模式进行抽象。λ-演算的高阶机制和重写的模式匹配功能在同一级别上都是可用的。λ-微积分的许多类型系统都可以推广到ρ-微积分：本文广泛地研究了一阶ρ-微积分。类型系统允许输入（面向对象的）固定点，从而导致一个表达和安全的演算。特别是，使用模式匹配，可以以自然和自动的方式对术语重写系统进行编码和类型检查。因此，我们可以将我们的框架视为强大的基于类型重写的语言的理论基础的起点。
The rewriting calculus, also calledρ-calculus, is a framework embeddingλ-calculus and rewriting capabilities, by allowing abstraction not only on variables but also on patterns. The higher-order mechanisms of theλ-calculus and the pattern matching facilities of the rewriting are then both available at the same level. Many type systems for theλ-calculus can be generalized to theρ-calculus: in this paper, we study extensively a first-orderρ-calculusà laChurch, called. The type system ofallows one to type (object oriented flavored) fixpoints, leading to an expressive and safe calculus. In particular, using pattern matching, one can encode and typecheck term rewriting systems in a natural and automatic way. Therefore, we can see our framework as a starting point for the theoretical basis of a powerful typed rewriting-based language.