Draft:Definitional tree

• Comment: You are writing this backwards, meaning you writing with what you know then trying to fill in sources that might support your knowledge. See WP:BACKWARD. Start over. You need to use reliable sources that have no affiliation with you and summarize what they say with no editiorizing. S0091 (talk) 21:06, 14 July 2025 (UTC)

---

In mathematics and computer science, a definitional tree is a tree data structure used in the evaluation of expressions by rewriting. Definitional trees are instrumental in finding needed evaluation steps. This is notable because unless every needed step of an expression is eventually executed, the value of the expression cannot be obtained.

Background

The rewriting systems considered in this note follow the constructor discipline. The signature of a system is partitioned into two sets: the data constructors (constructors for short) and the defined operations (operations or functions for short). The intuition is that expressions made only of constructors represent data whereas operations represent functions. Rewriting systems that obey the constructor discipline are also called constructor systems.

In constructor systems, the rewrite rules of an operation define the behavior of the operation applied to data values. More formally, the constructor discipline requires the left-hand side of a rewrite rule to be a pattern, i.e., an expression in which the root is an operation symbol, and the children of the root are expressions consisting of constructor symbols and/or variables only. Patterns are linear, i.e., any variable has at most one occurrence in a pattern.

Types are marginal to the definitional trees. Without further consideration, we establish that all the expressions discussed in this article are well-typed.

Example 1

Rewrite rules of the ordinary addition operator on natural numbers in unary notation and graphical representation of the corresponding definitional tree.

The following rewrite rules define a rewrite system. The system implicitly assumes the existence of a type, Nat. The system's signature consists of three symbols whose types are inferred from the context. 0 is a constructor of type Nat, s is a constructor from Nat to Nat and + is an operation (denoted infix) from Nat$\times$Nat to Nat:

0    + y -> y
s(x) + y -> s(x + y)

The intuition is that an expression consisting of 0 and s stands for a natural number in unary notation, e.g., s(s(0)) stands for 2, and + is the familiar addition operator, e.g., s(s(0))+s(s(0)) evaluates, in a few steps, to s(s(s(s(0)))), i.e., 4.

Definition

We assume an arbitrary, but fixed, ordering among the constructors of any type.

The nodes of a definitional tree come in three variants called branch, rule, and exempt. Any node, regardless of the variant, contains a pattern denoted by $\pi$ and possibly other information as follows:

• $exempt(\pi )$, no other information beside the pattern;
• $rule(\pi ,l\to r)$, where $l\to r$ is a rule and $\pi$ and $l$ are equal except for a renaming of the variables;
• $branch(\pi ,v,T_{1}\ldots T_{n})$, where $v$ is a variable of $\pi$ called inductive, and $T_{i}$ is a definitional tree with a pattern $\pi '$ such that $\pi '$ is equal to $\pi$ except that $v$ is replaced by $c_{i}(v_{1},\ldots v_{k})$, where $c_{i}$ is the $i^{th}$ constructor of the type of $v$, $k$ is its arity, and $v_{i}$ is a fresh variable, for all appropriate $i$.

A definitional tree $T$ of an operation $f$ is a definitional tree with the following requirements:

• The pattern in the root of $T$ is $f(x_{1},\ldots ,x_{n})$ where, for all appropriate $i$, $x_{i}$ is a fresh variable;
• The rule nodes of $T$ contain all and only the rules of $f$;
• Below every branch node of $T$ there is a rule node.

Exempt nodes occur in the definitional trees of incompletely defined operations, e.g., the operation that computes the head of a list. Such operation is not defined when the argument is the empty list.

Example 2

The textual representation of the definitional tree of the operation + presented in Example 1 is:

$branch(v_{1}+v_{2},v_{1},rule(0+v_{3},0+x\to x),rule(s(v_{4})+v_{5},s(x)+y\to s(x+y)))$

Definitional trees have a graphical representation that eases understanding. The names of the variables in a pattern are irrelevant. Hence all the variables are denoted by the same symbol, $\scriptstyle \square$, with the convention that each occurrence is unique. The inductive variable contained in any branch node is represented by $\scriptstyle \blacksquare$ in the pattern. We assume an arbitrary, but fixed, ordering among the rewrite rules of an operation. The rule in a rule node is represented by the rule index in this ordering.

Evaluation

Rewrite rules of operation take and corresponding definitional tree. Operation take takes a list $l$ and a natural number $n$ and returns either the list of the first $n$ elements of $l$ or the entire $l$, if $l$ has less than $n$ elements. Natural numbers are represented in unary notation. Lists are represented in the notation of the programming language Haskell. Likewise, symbol application is curried.

An operation $f$ is called inductively sequential if there exists a definitional tree of $f$. There are operations that do not have any definitional tree, e.g., the parallel or, and operations that have more than one. In this case, any tree can be used by the evaluation algorithm discussed below.

Rewriting systems in which every operation is inductively sequential are called inductively sequential as well and support the optimal, sequential evaluation strategy presented below.

Procedure needed, presented in annotated, Algol-like pseudo-code below, implements the algorithm to compute a needed redex of an expression $t$. Without loss of generality assume that $t$ is an expression rooted by an operation. The call needed$(t)$ either finds both a needed redex of $t$, if one there exists, and a rule to reduce it, or determines that $t$ has no value. A value of an expression, $t$, is a expression derived from $t$ and consisting of constructor symbols only.

procedure needed($t$): assumption: $t$ is an expression rooted by an operation procedure traverse($T$): let $\pi$ be the pattern of $T$ invariant: $t$ is an instance of $\pi$ case $T$ of: $rule(\pi ,l\to r)$: output $t$ is a needed redex reducible by $l\to r$ $exempt(\pi )$: output $t$ has no value $branch(\pi ,v,T_{1}\ldots T_{n})$: if $t$ is an instance of the pattern of $T_{i}$, for some $i$: then traverse($T_{i}$) else needed($t'$), where $t'$ is the match of $v$ traverse($T$), where $T$ is a definitional tree of the root of $t$

Procedure traverse, nested within procedure needed, has access to its local variable, $t$. Informally, the algorithm works as follows. Given an expression $t$ of the form $f(t_{1},\ldots ,t_{n})$, where $f$ is a function symbol of arity $n$ and $t_{i}$ is some expression for all appropriate $i$, find in the definitional tree of $f$ a deepest node, say $N$, whose pattern matches $t$. There always exists exactly one such node. If $N$ is a branch node, then the match of the inductive variable is a subexpression of $t$, say $t'$, rooted by a function symbol. Unless this expression is reduced to an expression rooted by a constructor symbol, no rule can be applied to $t$. Hence, the recursive call. If $N$ is a rule node, then $t$ is a needed redex reducible by the rule of $N$. If $N$ is an exempt node, then $t$ has no value.

Properties

Definitional trees have been invented by S. Antoy in 1992.

The inductively sequential rewriting systems are the intersection of the constructor systems and the strongly sequential systems. Hence, the inductively sequential systems are the largest constructor class in which needed redexes are computable.

Definitional trees define the operational semantics of the functional logic programming languages ${\mathcal {TOY}}$ and Curry.