Infinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Boehm tree in the lambda calculus. It was first introduced in [AB97] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrit e system. In [Blo01] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach.

Grammars and rewriting systems (msc 68Q42), Semantics (msc 68Q55)
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Blom, S.C.C. (2002). Lifting infinite normal form definitions from term rewriting to term graph rewriting. Software Engineering [SEN]. CWI.