Sciweavers

ENTCS
2007

Hierarchical Nominal Terms and Their Theory of Rewriting

13 years 10 months ago
Hierarchical Nominal Terms and Their Theory of Rewriting
Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasingly ‘meta-level’ variables, e.g. in hierarchical nominal term rewriting the meta-level unknowns (representing unknown terms) in a rewrite rule can be ‘folded into’ the syntax itself (and rewritten). To the extent that rewriting is a mathematical metaframework for logic and computation, and nominal rewriting is a framework with native support for binders, hierarchical nominal term rewriting is a meta-to-the-omega level framework for logic and computation with binders.
Murdoch Gabbay
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Murdoch Gabbay
Comments (0)