Relative Normalization in Higher-Order Rewriting Systems

John Glauert

School of Information Systems, UEA

Norwich NR4 7TJ England J.Glauert@uea.ac.uk

Zurab Khasidashvili NTT Basic Research Laboratories Atsugi, Kanagawa 243-01 Japan zurab@theory.brl.ntt.jp ^{∗}

Abstract

The Abstract.

1 Picture

Consider an OTRS R = {f(x) → g(x, h(x)), h(x) → c, a → b} and a term (redex) u = f(a):

[figure: f(a); f; g(a, h(a)); f; g(a, c)]

[figure: g(b, h(a)); a; g(a, h(b)); h; a] [figure: f(b); a; f; g(b, h(b)); h; a; a; g(b, c); a; h] ∗Part of this work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H 41300.

Consider an OTRS R = {f(x) → g(x, h(x)), h(x) → c, a → b} and a term (redex) u = f(a):

f(a)  \overline{}g(a, h(a))

[figure: g(b, h(a)); g(a, h(b)); g(a, c)]

[figure: f(b); g(b, h(b)); g(b, c)]