zbMATH — the first resource for mathematics

The simply typed rewriting calculus. (English) Zbl 0962.68084
Futatsugi, Kokichi, The 3rd international workshop on rewriting logic and its applications, RWLW. Kanazawa City Cultural Hall, Kanzawa, Japan, September 18-20, 2000. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 36, 19 p., electronic only (2000).
Summary: The rewriting calculus is a rule construction and application framework. As such it embeds in a uniform way term rewriting and lambda-calculus. Since rule application is an explicit object of the calculus, it allows us also to handle the set of results explicitly. We present a simply typed version of the rewriting calculus. With a good choice of the type system, we show that the calculus is type preserving and terminating, i.e. verifies the subject reduction and strong normalization properties.
For the entire collection see [Zbl 0957.00046].

68Q42 Grammars and rewriting systems
68N18 Functional programming and lambda calculus
Full Text: Link