Typically, the terminal algebra is just the domain of strings over an alphabet, together with the binary concatenation operator and the usual identity laws for strings: concatenation is associative, is a left and right identity.
An unbound rule is a construction of the form
where n 0, the v are distinct variables, the t are answers (usually, but not necessarily, terminal), and the e are polynomials in the variables v.
The ordered pairs in an unbound rule, v,e and all e,v , are called unbound pairs. The left-hand component of each pair plays the same meta-syntactic role as a Christiansen language attribute. The t on the right side of the rule act as syntax. The right-hand component of each pair is usually interpreted as capturing the semantics of the terminal string generated by that pair.
The domain of unbound rules is related to the domain of answers by means of a rule function, . When binding the variables of an unbound rule r as above, the leftmost variable v must be bound to some answer a A such that r (a). This is equivalent to Christiansen's requirement that the rule used to expand each parent node of the parse tree must be drawn from the language attribute of that node.
The rule function determines the meta-syntactic sense of each answer. Nonterminal constants, i.e., nonterminal operators of arity zero, have a fixed meta-syntactic sense, just as nonterminals in CFGs. The unique nature of the rule function comes from the way it handles terminals, and non-constant nonterminal operators.
For all terminals t in a RAG G, ( t ) = { v, t }. In other words, when a terminal is used as meta-syntax, it generates the singleton language containing itself, and "synthesizes" semantic value .
For each nonterminal non-constant operator of arity n 1 in a RAG G, there is a rule equation that defines (( . . . )) as a function of the arguments to . Here is a canonical example.
This rule equation defines the meta-syntactic behavior of the binary infix + operator. It says, in essence, that for all answers a and b, the answer a+b generates the union of the languages generated by the two arguments. This particular operator is called the union operator.
The design goal of nontrivial expression evaluation is addressed by the introduction of a special binary operator called the query operator, written a:b, that denotes a semantic value associated by meta-syntactic value a with syntactic value b. That is,
Proposition 0.1 For all a,b,c A, a:b c iff a,c b.Technically, the query operator does not belong to the answer algebra. It belongs to a larger algebra Q, called the query algebra, of which A is a proper subalgebra. The polynomials in an unbound rule are expressions over the query algebra, hence they can use the query operator.
In Proposition 0.1, the two derivations are, so to speak, working in opposite directions. The first derivation may be thought of as constructing a parse tree from the bottom up, while the second derivation constructs the same tree from the top down. Since the derivation relation is merely the transitive closure of a step relation , the step relation must somehow implement this kind of bi-directional behavior.
This is accomplished in the RAG model by introducing yet another special operator, this time a unary operator called the inverse operator and written . The inverse operator does not belong to the query algebra; it belongs to the configuration algebra, C, of which Q is a proper subalgebra. The configuration algebra also includes the binary pairing operator, ,, which is used to form the ordered pairs in unbound rules. Formally, the derivation step is a relation between configurations.
Algebraically, the inverse of an answer is that answer, i.e., a = , while the inverse of the inverse of any configuration is that configuration, i.e., c = . The inverse operator figures prominently — and often subtly — in most of the axioms that define the derivation step relation; the most basic example is:
Axiom 0.1 For all c,d C, c d iff .Thus, for example, for all a A, c a implies = a .
Proposition 0.1 falls out as a relatively straightforward consequence of these derivation step axioms. Another consequence of the same axioms is that, for all answers a,b A, a b implies a = b. Despite the simplicity of the latter result, its proof is highly nontrivial.
A RAG is strongly stepwise decidable iff (1) the rule function can be computed by a Turing machine, and (2) given any two polynomials over the configuration algebra, a Turing machine can decide whether they are identically equal. Neither of these conditions is guaranteed by the general definition of RAGs. If both conditions hold for a RAG G, then it is possible to construct a Turing machine that decides, for any two configurations c and d, whether or not c d.
Intuitively, weak answer-encapsulation means that when two answers have the same "interface", they cannot be told apart by formal means. The notion of interface is expressed, for a RAG G, by an equivalence relation over A, such that a b iff a and b generate the same syntax, and assign equivalent semantics to that syntax. More precisely, for all x,x',y,z A, if x x' and x:y z then there exists z' A such that z z' and x':y z'. An operator on A is G-safe iff it preserves answer-equivalence; G is weakly answer-encapsulated iff all of the operators on A are G-safe (that is, formally, iff is a congruence on A).
Strong answer-encapsulation extends the concept of operator safeness to classes of RAGs. Rule equations, such as the one given earlier for the union operator, are used to define the generic behavior of a set of operators, independent of any specific RAG that satisfies those equations. A collection of rule equations , called a framework, is safe iff, for all possible RAGs G that satisfy , and all operators defined by , is guaranteed to be G-safe. A RAG G is strongly answer-encapsulated iff there exists some safe framework that is satisfied by G and defines all of the operators on A.
All of the RAG frameworks used in this thesis are safe. However, the general problem of determining whether a framework is safe seems to be rather complicated, with large numbers of exceptions and special cases. In practice, it is convenient to use a combination of general and specific proof techniques. Almost all of the frameworks in the thesis are covered by a small group of moderately general framework safety theorems; only three operators are not covered, and these are easily handled on an individual basis.
It may be noted, in passing, that there exist rule equations that are inherently unsafe, in the sense that no framework containing such an equation can possibly be safe.
A RAG is well-behaved iff it is both strongly stepwise decidable and strongly answer-encapsulated. The well-behaved RAG model is Turing-powerful. Formally, to every Turing machine M that accepts language L and computes partial function f, there exists a well-behaved RAG G that generates language L, and assigns to each string w L the semantic value f(w).