Hubbry Logo
Normal form (abstract rewriting)Normal form (abstract rewriting)Main
Open search
Normal form (abstract rewriting)
Community hub
Normal form (abstract rewriting)
logo
7 pages, 0 posts
0 subscribers
Be the first to start a discussion here.
Be the first to start a discussion here.
Contribute something
Normal form (abstract rewriting)
Normal form (abstract rewriting)
Normal form (abstract rewriting)
View on Wikipedia
from Wikipedia

In abstract rewriting,[1] an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.

Definitions

[edit]

Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term.

An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form. A rewriting system has the weak normalization property or is (weakly) normalizing (WN) if every object is weakly normalizing. An object a is strongly normalizing if every sequence of rewrites starting from a eventually terminates with a normal form. A rewriting system is strongly normalizing, terminating, noetherian, or has the (strong) normalization property (SN), if each of its objects is strongly normalizing.[2]

A rewriting system has the normal form property (NF) if for all objects a and normal forms b, b can be reached from a by a series of rewrites and inverse rewrites only if a reduces to b. A rewriting system has the unique normal form property (UN) if for all normal forms a, b ∈ S, a can be reached from b by a series of rewrites and inverse rewrites only if a is equal to b. A rewriting system has the unique normal form property with respect to reduction (UN→) if for every term reducing to normal forms a and b, a is equal to b.[3]

Results

[edit]

This section presents some well known results. First, SN implies WN.[4]

Confluence (abbreviated CR) implies NF implies UN implies UN→.[3] The reverse implications do not generally hold. {a→b,a→c,c→c,d→c,d→e} is UN→ but not UN as b=e and b,e are normal forms. {a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.

WN and UN→ imply confluence. Hence CR, NF, UN, and UN→ coincide if WN holds.[5]

Examples

[edit]

One example is that simplifying arithmetic expressions produces a number - in arithmetic, all numbers are normal forms. A remarkable fact is that all arithmetic expressions have a unique value, so the rewriting system is strongly normalizing and confluent:[6]

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24
(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 ⇒ 2 ⇒ 3 ⇒ ...) and loops such as the transformation function of the Collatz conjecture (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., it is an open problem if there are any other loops of the Collatz transformation).[7] Another example is the single-rule system { r(x,y) → r(y,x) }, which has no normalizing properties since from any term, e.g. r(4,2) a single rewrite sequence starts, viz. r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., which is infinitely long. This leads to the idea of rewriting "modulo commutativity" where a term is in normal form if no rules but commutativity apply.[8]

Weakly but not strongly normalizing rewrite system[9]

The system {b → a, b → c, c → b, c → d} (pictured) is an example of a weakly normalizing but not strongly normalizing system. a and d are normal forms, and b and c can be reduced to a or d, but the infinite reduction b → c → b → c → ... means that neither b nor c is strongly normalizing.

Untyped lambda calculus

[edit]

The pure untyped lambda calculus does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term (application is left associative). It has the following rewrite rule: For any term ,

But consider what happens when we apply to itself:

Therefore, the term is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.

Typed lambda calculus

[edit]

Various systems of typed lambda calculus including the simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are strongly normalizing.

A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete, otherwise one could solve the halting problem by seeing if the program type checks. This means that there are computable functions that cannot be defined in the simply typed lambda calculus, and similarly for the calculus of constructions and System F. A typical example is that of a self-interpreter in a total programming language.[10]

See also

[edit]

References

[edit]
Revisions and contributorsEdit on WikipediaRead on Wikipedia

Normal form (abstract rewriting)

View on Grokipedia
from Grokipedia
In abstract rewriting theory, a normal form of an element xx in a is an yy such that xx reduces to yy in zero or more steps, where irreducibility means no further one-step reduction is possible from yy. An , or ARS, provides the foundational framework for this concept and is formally defined as a pair (A,→)(A, \rightarrow), where AA is a set (often countable) and →⊆A×A\rightarrow \subseteq A \times A is a denoting one-step reductions. Elements of AA represent states or terms, and a reduction a→ba \rightarrow b indicates a transformation from aa to bb. The reflexive-transitive closure of →\rightarrow, denoted →∗\rightarrow^* or  ⁣→\! \rightarrow, captures multi-step reductions, allowing normal forms to be reached through sequences of such steps. Normal forms are central to analyzing the behavior of systems, particularly in assessing termination and equivalence of elements. A is normalizing if every element has at least one normal form (weak normalization), and strongly normalizing (or terminating) if all reduction sequences from any element are finite and thus end in a normal form. Uniqueness of normal forms arises under (also known as the Church-Rosser property), which ensures that any two elements reachable by different reduction paths from a common ancestor can be joined by further reductions to a shared descendant; in confluent and normalizing systems, this guarantees a unique normal form for each element. A that is both confluent and terminating is called convergent or , enabling effective computation of the canonical (unique) normal form to decide equality. These properties underpin applications in , such as , languages like (via reductions), and algebraic simplification, where reducing expressions to normal forms facilitates optimization and verification. However, not all systems possess normal forms—non-terminating reductions may lead to infinite chains without reaching irreducibility—and uniqueness requires additional structural conditions like .

Fundamentals of Abstract Rewriting

Abstract Rewriting Systems

An abstract rewriting system (ARS), also known as an abstract reduction system, is a fundamental mathematical structure in theoretical computer science and mathematical logic, consisting of a set AA and a binary relation →\to on AA, where →\to represents the one-step rewrite or reduction steps between elements of AA. More generally, an ARS can involve a family of binary relations {→i}i∈I\{ \to_i \}_{i \in I} on AA, allowing for multiple types of reduction rules, though the single-relation case is often sufficient for basic analysis. This pair is denoted as A=⟨A,→⟩A = \langle A, \to \rangle, capturing the essence of rewriting without specifying the nature of the elements in AA or the concrete form of the reductions. The →\to in an ARS defines immediate transformations, while the reflexive-transitive closure →∗\to^* extends this to sequences of zero or more such steps, representing multi-step reductions from one element to another. This closure is crucial for studying longer reduction paths, such as those forming reduction sequences where an element aa reduces to bb if a→∗ba \to^* b. In contrast to concrete implementations, an abstract ARS remains purely relational and set-theoretic, without presupposing structure on AA; for instance, string systems apply ARS to alphabets of symbols with , while term systems use ARS on terms built from function symbols and variables via substitution and application. The concept of ARS originated with M. H. A. Newman's work on theories defined by combinatorial equivalence, where he introduced reduction systems to analyze graph-based transformations and equivalence relations induced by reductions. In the 1980s, Jan Willem Klop generalized this framework in his study of combinatory reduction systems, extending ARS to encompass and other higher-order rewriting paradigms, thereby unifying diverse computational models under a common abstract theory.

Basic Reduction Concepts

In an (ARS), defined as a pair (A,→)(A, \to) where AA is a set and →⊆A×A\to \subseteq A \times A is a , reductions capture the process of transforming elements through successive applications of rewrite rules. The one-step reduction relation →\to denotes a direct, single transformation from an element a∈Aa \in A to b∈Ab \in A, written a→ba \to b, if (a,b)∈→(a, b) \in \to. This represents the immediate effect of applying a single rewrite rule to aa, yielding bb as its direct reduct. In contrast, the multi-step reduction relation →∗\to^* is the reflexive of →\to, allowing zero or more such steps; thus, a→∗ba \to^* b if there exists a finite sequence a=a0→a1→⋯→an=ba = a_0 \to a_1 \to \cdots \to a_n = b for some n≥0n \geq 0. The multi-step relation encompasses both trivial reductions (where a→∗aa \to^* a with n=0n=0) and chains of arbitrary finite length, providing a way to describe extended paths in the . Reduction sequences are chains of elements connected by →\to steps, such as a0→a1→a2→⋯a_0 \to a_1 \to a_2 \to \cdots. These sequences may be finite, terminating after a fixed number of steps (e.g., a0→a1→a2a_0 \to a_1 \to a_2 with no further reduction specified), or infinite, continuing indefinitely without end (e.g., a0→a1→a2→⋯a_0 \to a_1 \to a_2 \to \cdots). Finite sequences model computations that halt, while infinite ones indicate non-terminating behavior, such as loops in the reduction process. In the reduction graph of an ARS—a with vertices AA and edges corresponding to →\to—these sequences appear as paths, highlighting the connectivity and potential cycles within the system. Peak and valley configurations arise in the structure of these reduction graphs and illustrate local divergence or convergence in reductions. A peak occurs when a single element v∈Av \in A has two distinct one-step reducts, forming u←v→wu \leftarrow v \to w where u≠wu \neq w; this represents a branching point where reduction can proceed in multiple directions from vv. Conversely, a valley is a configuration u→∗v←wu \to^* v \leftarrow w, where two elements uu and ww both reach a common reduct vv via multi-step reductions; it signifies a merging of paths after possible divergence. These structures are fundamental to analyzing the flow of reductions without implying global properties like joinability. The →∗\to^* inherits key properties from its construction as the reflexive of →\to. Reflexivity holds because every a∈Aa \in A satisfies a→∗aa \to^* a via the zero-step sequence, ensuring that elements are trivially related to themselves. Transitivity is satisfied since if a→∗ba \to^* b and b→∗cb \to^* c, then the concatenated sequence yields a→∗ca \to^* c, allowing reductions to compose seamlessly along paths. These properties make →∗\to^* a on AA, facilitating the study of reduction orderings and chains. In general, →\to itself need not be reflexive or transitive, but its closure →∗\to^* always is.

Definition and Properties of Normal Forms

Formal Definition

In an abstract reduction system ⟨A,→⟩\langle A, \to \rangle, where AA is a set and →⊆A×A\to \subseteq A \times A is a , an element t∈At \in A is in normal form if there exists no s∈As \in A such that t→st \to s. Such an element tt is also termed irreducible. A normal form of an element x∈Ax \in A is an y∈Ay \in A such that x→∗yx \to^* y, where →∗\to^* denotes the of →\to. Equivalently, tt is a →∗\to^*-minimal element. The collection of all normal forms is given by the set NF(A,→)={t∈A∣∀s∈A. ¬(t→s)}.\mathrm{NF}(A, \to) = \{ t \in A \mid \forall s \in A.\ \neg (t \to s) \}. In typed contexts such as , which can be viewed as specific instances of abstract reduction systems on terms, restricted notions like head normal form and weak head normal form arise; these require irreducibility only at the outermost (head) position of the term, allowing potential reductions in subterms.

Irreducibility and Uniqueness

In an abstract rewriting system (ARS), irreducibility constitutes the fundamental property of a normal form, indicating that no one-step reduction is possible from the term. This means there exists no other element to which the term can directly reduce, distinguishing normal forms from reducible terms that admit further transformations. Uniqueness of normal forms is not assured in arbitrary ARS; a given term may possess multiple distinct normal forms depending on the chosen reduction path. However, this uniqueness is guaranteed when the system satisfies the confluence property, ensuring all reduction sequences from a term converge to the same irreducible element. To illustrate non-uniqueness, consider a simple ARS with elements {a,b,c}\{a, b, c\} and reduction rules a→ba \to b, a→ca \to c, where bb and cc admit no further . Here, aa reduces to two different normal forms, bb and cc, highlighting the absence of .

Key Theoretical Results

Confluence and Church-Rosser Theorem

In abstract rewriting systems, local confluence, also known as the weak property, is defined as follows: for any terms uu, vv, and ww such that u→vu \to v and u→wu \to w, there exists a term xx such that v→∗xv \to^* x and w→∗xw \to^* x. This ensures that single-step reductions from a common ancestor can be joined after finitely many steps. , often referred to as the strong or the Church-Rosser in this context, extends this idea globally: for any terms uu, vv, and ww such that u→∗vu \to^* v and u→∗wu \to^* w, there exists a term zz such that v→∗zv \to^* z and w→∗zw \to^* z. In a confluent , distinct reduction paths from the same starting term eventually meet, which is crucial for the uniqueness of normal forms when they exist. Newman's lemma establishes a key connection between local confluence and global confluence under the assumption of termination: if a rewriting relation is terminating and locally confluent, then it is . This result, originally proved in the context of combinatorial equivalence relations, has become fundamental in abstract theory. The Church-Rosser theorem states that a is if and only if it satisfies the Church-Rosser property, meaning that two terms are joinable (i.e., have a common reduct) precisely when they are convertible via symmetric closure of the reduction relation. In such systems, if a term reduces to , that normal form is unique regardless of the reduction path taken. A sketch of the proof linking these concepts begins with the diamond property characterizing local confluence, where overlapping single reductions join immediately. For global confluence, the union lemma combines local joins along reduction sequences, and termination ensures no infinite descending chains prevent the process from completing.

Normalization and Termination

In abstract reduction systems (ARS), termination is a fundamental property that guarantees the finiteness of all reduction sequences, ensuring that normal forms exist and can be reached. An ARS (A,→)(A, \to) is terminating if there exists no infinite sequence a0→a1→a2→⋯a_0 \to a_1 \to a_2 \to \cdots with all ai∈Aa_i \in A. This property, equivalently known as strong normalization when applied to individual elements, implies that every reduction path starting from any element a∈Aa \in A eventually reaches an (normal form). A related but weaker condition is weak normalization, where for every a∈Aa \in A, there exists at least one finite reduction sequence a→∗ba \to^* b such that bb is a normal form, though other sequences from aa may be infinite. Strong normalization implies weak normalization, as the absence of infinite paths ensures that all terminating paths end in normal forms, but the converse does not hold—systems can be weakly normalizing without being strongly normalizing if some paths diverge. Termination can be established using well-founded orders on AA, where reductions strictly decrease with respect to the order. In the specific context of term rewriting systems (TRS), which are ARS restricted to terms over a , the Knuth–Bendix completion procedure provides a method to derive a and terminating rewrite system from an initial set of equations. Given a finite set of equations, the algorithm iteratively orients them into rewrite rules using a reduction ordering and adds new rules from critical pairs until no overlaps remain, yielding a complete system if the process terminates; this ensures both (for unique normal forms) and termination. The procedure's success relies on selecting an appropriate terminating ordering, such as a simplification ordering, to orient rules and prevent infinite computations during completion. Not all ARS terminate, and non-termination arises when infinite reduction chains exist, precluding normal forms for affected elements. For instance, consider an ARS on the natural numbers N\mathbb{N} with the reduction n→n+1n \to n+1 for all n∈Nn \in \mathbb{N}; this forms an infinite ascending chain from any starting number, rendering the system non-terminating with no normal forms. Similarly, unrestricted reductions in , such as those involving fixed-point combinators like the , can produce perpetual loops, as in the reduction of Y applied to a non-terminating functional, leading to infinite sequences without convergence to .

Examples in Rewriting Systems

Untyped Lambda Calculus

The untyped serves as a concrete instance of an (ARS), where lambda terms form the set of objects and β-reduction defines the rewrite relation. In this framework, a term is rewritten by substituting the argument of an application into the body of a lambda abstraction, specifically via the rule (λx.M)N→βM[x:=N](λx.M)N \to_β M[x := N], where the substitution is capture-avoiding (achieved by alpha-renaming the bound variable if necessary to prevent free variables in N from being captured by binders in M). This relation captures the computational essence of without type restrictions, allowing terms to represent arbitrary functions and computations. A term in the untyped is in β-normal form if it contains no β-redexes, meaning no subterm of the form (λx.M)N(λx.M)N that can undergo further β-reduction. Such normal forms include basic abstractions like variables or applications where the operator is not a , as well as more complex encodings such as Church numerals, which represent natural numbers as higher-order functions—for instance, the numeral for 2 is λf.λx.f(fx)\lambda f.\lambda x. f(fx), applying ff twice to xx. Combinators, which are closed terms without free variables, also often appear in β-normal form; examples include the identity combinator I=λx.xI = \lambda x.x and the constant combinator K=λx.λy.xK = \lambda x.\lambda y.x. These encodings demonstrate how the untyped system supports expressive representations of data and operations while adhering to the irreducibility of normal forms. Not all terms possess a β-normal form, as illustrated by the non-terminating example Ω=(λx.xx)(λx.xx)\Omega = (\lambda x.xx)(\lambda x.xx), which reduces to itself indefinitely: Ω→βΩ→βΩ⋯\Omega \to_β \Omega \to_β \Omega \cdots, forming an infinite reduction sequence with no irreducible term. This highlights the untyped lambda calculus's lack of normalization, where some computations diverge rather than terminating in a normal form. To reach a β-normal form when it exists, various reduction strategies guide the order of β-reductions. , or leftmost-outermost reduction, prioritizes the outermost redex on the left, substituting arguments into the function body before reducing the arguments themselves; this strategy is normalizing, meaning it always finds if one exists. In contrast, applicative order, or rightmost-innermost reduction, fully reduces arguments to normal form before applying the function, which may lead to non-termination even when is available, as in cases involving divergent arguments like Ω\Omega. Both strategies respect the system's confluence but differ in efficiency and termination guarantees. The Church-Rosser theorem applies specifically to the untyped under β-reduction, stating that if a term PP reduces to both QQ and RR, then there exists a term SS such that QQ reduces to SS and RR reduces to SS; this ensures that any β-normal form of a term is unique up to α-equivalence (renaming of bound variables). Proved originally by Church and Rosser, the theorem underscores the system's , implying that different reduction paths converge to the same normal form, thereby validating the consistency of computations in this ARS.

Term Rewriting Systems

A term rewriting system (TRS) is a typed consisting of a Σ\Sigma, which includes a of function symbols each with a specified , and a of variables VV. The set of terms T(Σ,V)T(\Sigma, V) is defined inductively: variables are terms, and if f∈Σf \in \Sigma has nn, then f(t1,…,tn)f(t_1, \dots, t_n) is a term for any terms t1,…,tn∈T(Σ,V)t_1, \dots, t_n \in T(\Sigma, V). Ground terms T0(Σ)T_0(\Sigma) form the subset with no variables. A rewrite rule is a pair l→rl \to r of non-variable terms where every variable occurring in rr also occurs in ll, and the TRS is the pair (Σ,R)(\Sigma, R) with RR a finite or infinite set of such rules. In a TRS, a term tt is in normal form if no rule in RR applies to any subterm of tt, meaning tt has no redex (reducible expression). Ground normal forms, which are normal forms in T0(Σ)T_0(\Sigma), play a key role in equational reasoning, such as for group axioms (e.g., associativity, identity, and inverses), where rules are oriented from the axioms to form a TRS that decides equality by reduction to a unique ground normal form representing each . Confluence in TRS ensures that distinct reduction paths from a term lead to the same normal form, enabling unique normal forms. The critical pair theorem provides a criterion for local confluence: a TRS is locally confluent if and only if every critical pair—arising from unifying the left-hand side of one rule with a non-variable subterm of another's left-hand side, then applying the rules—is joinable, meaning the resulting terms have a common reduct. For terminating TRS, local confluence implies global confluence by Newman's lemma. A representative example is the associativity rule (x⋅y)⋅z→x⋅(y⋅z)(x \cdot y) \cdot z \to x \cdot (y \cdot z) over a with binary ⋅\cdot. Left-associated terms like ((a⋅b)⋅c)((a \cdot b) \cdot c) reduce to a⋅(b⋅c)a \cdot (b \cdot c), which is irreducible and thus ; more generally, fully right-associated terms are the normal forms under this rule. The Knuth-Bendix completion algorithm constructs a confluent TRS from an initial set of unoriented equations EE over Σ\Sigma by selecting a total, stable reduction ordering >> on terms, orienting each equation s=ts = t in EE as s→ts \to t or t→st \to s with s>ts > t, and iteratively computing and resolving critical pairs: if a pair ⟨u,v⟩\langle u, v \rangle is not joinable, add the oriented equation u=vu = v to EE and repeat until no new critical pairs arise or termination fails, yielding a complete TRS with unique normal forms for terms provably equal under EE.
Add your contribution
Related Hubs
Contribute something
User Avatar
No comments yet.