Definition. Compositionality, computability, and complexity › Term rewrite systems (§ 6.1) [pagin2021-trs]

A term rewrite system (TRS) Φ is a pair ⟨ΣΦ,RΦ⟩ where—

  1. ΣΦ is a signature comprising a finite set of n-ary operators (including nullary constants), and
  2. RΦ is a set of reductions over the set TΦ of terms over ΣΦ.

We will write t1→Φt2 (omitting the subscript where context makes it obvious) when the application of some rule r∈RΦ yields the contractum t2.

A sequence of applications t1→t2→...→tn is a derivation. We write t1→Φ+tn where →Φ+ is the transitive closure of →.

Definition 1. Conditional term rewrite systems (§ 6.1) [pagin2021-ctrs]

In a conditional term rewrite system ΣΦ,RΦ, the reductions are conditioned over some conditions C1,...,Cn.

Definition 2. Many-sorted term rewrite systems (§ 6.1) [pagin2021-many-sorted-trs]

In a many-sorted term rewrite system, TPsi is partitioned into subsets corresponding to sorts, and argument places for operators have sort restrictions; complex terms whose subterms satisfy the sort restrictions are well-sorted (corresponding to grammaticality).

Definition 3. Normal form (§ 6.1) [pagin2021-normal-form]

A term that cannot be reduced further is in normal form.

Definition 4. Termination (§ 6.1) [pagin2021-terminate]

If every derivation leads to a term in normal form, a system terminates.

Definition 5. Confluence (§ 6.1) [pagin2021-confluence]

Φ is confluent iff, for all terms t1,t2,t3, whenever t1→Φ+t2 and t1→Φ+t3, there is some t4 such that t2→Φ+t4 and t3→Φ+t4.

Definition 6. Convergence (§ 6.1) [pagin2021-convergence]

A confluent system that terminates is convergent.

Context

    Reference. Compositionality, computability, and complexity [pagin2021]

    Definition. Grammatical term algebra (§ 2.1) [pagin2021-gta]

    A grammatical term algebra GTAL of a language L is a partial algebra ⟨GTL,ATL,ΣL⟩, where—

    1. GTL is the set of grammatical terms for L,
    2. ATL is a finite set of atomic (grammatical) terms for L, and
    3. ΣL is a finite set of syntactic operations for L. GTL is the closure of ATL under ΣL.

    Definition. Meaning operations (§ 2.2) [pagin2021-meaning-operation]

    A meaning operation r over a domain of meanings M is some function Mn→M.

    Definition. Semantic functions (§ 2.2) [pagin2021-semantic-function]

    Where GTAL is a grammatical term algebra and M is a domain of meanings, any μ:GTL→M is a semantic function.

    Definition. Standard compositionality (§ 2.2) [pagin2021-standard-compositionality]

    Given a grammatical term algebra GTAL and domain M of meanings, a semantic function μ:GTL→M is standard compositional iff for every n-ary operation σ∈ΣL there is a meaning operation rσ:Mn→M such that for any t1,...,tn∈Domσ⊆GTL, μ(σ(t1,...,tn))=rσ(μ(t1),...,μ(tn)).

    Definition. General compositionality (§ 2.3) [pagin2021-general-compositionality]

    A semantic system S is general compositional iff for every n-ary operation σ∈ΣL and every member μi∈S′ there is a meaning operation Mn→M such that for any grammatical terms t1,...,tn∈Domσ μi(σ(t1,...,tn))=rσ,i(μj1(t1),...,μjn(tn)), where for 1⩽k⩽n μjk=ΦS(μi,σ,k).

    Definition. Meaning algebras (§ 3) [pagin2021-meaning-algebra]

    A meaning algebra over a set of meanings M is a triple MAM=⟨M,BM,RM⟩, where—

    1. BM is a finite set of basic meanings,
    2. RM is a finite set of elementary meaning operations,
    3. M closes BM under RM, and
    4. for all δ,δ′∈RM and x1,...xn,y1,...,ym, δ(x1,...,xn)∉BM and, if δ(x1,...,xn)=δ′(y1,...,ym) then δ=δ′, m=n, and xi=yi for 1⩽i⩽n.

    Definition. Semantic systems (§ 3) [pagin2021-semantic-system]

    Given a grammatical term algebra GTAL and domain M of meanings, a semantic system S is a triple ⟨S′,μS,ΦS⟩ where—

    1. S′ is a finite set of semantic functions μj:GTL→M, μS∈S, and
    2. ΦS:S′×ΣL×N→S′ is a partial selection function.

    Given some semantic function μj and a syntactic operation σ, ΦS then gives another semantic function μk for each nth-position term.

    Finally, S(t)=μS(t).

    Definition. Semantic algebras (§ 3) [pagin2021-semantic-algebra]

    A semantic algebra over a language L and domain M of meanings is a triple SALM=⟨⟨GTL,M⟩,⟨ATL,BM⟩,⟨ΣL,RM⟩⟩ where—

    1. ⟨GTL,ATL,ΣL⟩ is a grammatical term algebra for L, and
    2. ⟨M,BM,RM⟩ is a meaning algebra for M.

    Definition. Size (§ 5) [pagin2021-size]

    The size of a term is the number of atoms and operators contained within it.

    Definition. Input terms (§ 5) [pagin2021-input-terms]

    The input terms of a rewriting system are of the form ‘μ(t)’ where t is a syntactic term.

    Definition. Input complexity (§ 5) [pagin2021-input-complexity]

    Let s be a normal term.

    The term complexity CtR(s) of s relative to R is the length of the shortest derivation from some input term μ(t) to s.

    The input complexity CRi(k) is the maximal CtR(s) where s has size k.

    Definition. Term rewrite systems (§ 6.1) [pagin2021-trs]

    A term rewrite system (TRS) Φ is a pair ⟨ΣΦ,RΦ⟩ where—

    1. ΣΦ is a signature comprising a finite set of n-ary operators (including nullary constants), and
    2. RΦ is a set of reductions over the set TΦ of terms over ΣΦ.

    We will write t1→Φt2 (omitting the subscript where context makes it obvious) when the application of some rule r∈RΦ yields the contractum t2.

    A sequence of applications t1→t2→...→tn is a derivation. We write t1→Φ+tn where →Φ+ is the transitive closure of →.

    Definition. Conditional term rewrite systems (§ 6.1) [pagin2021-ctrs]

    In a conditional term rewrite system ΣΦ,RΦ, the reductions are conditioned over some conditions C1,...,Cn.

    Definition. Many-sorted term rewrite systems (§ 6.1) [pagin2021-many-sorted-trs]

    In a many-sorted term rewrite system, TPsi is partitioned into subsets corresponding to sorts, and argument places for operators have sort restrictions; complex terms whose subterms satisfy the sort restrictions are well-sorted (corresponding to grammaticality).

    Definition. Normal form (§ 6.1) [pagin2021-normal-form]

    A term that cannot be reduced further is in normal form.

    Definition. Termination (§ 6.1) [pagin2021-terminate]

    If every derivation leads to a term in normal form, a system terminates.

    Definition. Confluence (§ 6.1) [pagin2021-confluence]

    Φ is confluent iff, for all terms t1,t2,t3, whenever t1→Φ+t2 and t1→Φ+t3, there is some t4 such that t2→Φ+t4 and t3→Φ+t4.

    Definition. Convergence (§ 6.1) [pagin2021-convergence]

    A confluent system that terminates is convergent.

    Definition. μ-systems (§ 6.1) [pagin2021-mu-system]

    A μ-system is a pair Φ=⟨ΣΦ,RΦ⟩ where—

    1. Σ=⟨Σo,Σm⟩ (an object- and meta-language signature),
    2. Σo=⟨Ao,Σo′⟩ where Ao is a set of atomic terms and Σ′ is a set of n-ary syntactic operators, so that the closure To of AO under Σ′ yields the grammatical term algebra ⟨TO,AO,ΣO′⟩ of OL,
    3. Σm=⟨Am,Σm′,S,F,G⟩ where—
      1. Am is a nonempty set of atomic meta-language expressions,
      2. Σm′ is a nonempty set of meta-language syntactic operators,
      3. S is a nonempty set of elementary meta-language function symbols,
      4. F is a possibly empty set of meta-language recursive function symbols over object language terms, and
      5. G is a possibly empty set of meta-language recursive function symbols over meta-language terms.

    Remark. 

    The canonical expressions of ML, Cm, close Am under Σm′, canonically express meanings, do not contain any μ operators or F/G functors, and rewrite derivations terminate with them.

    Remark. 

    The set S of the semantic vocabulary of Φ contains at least the semantic function symbol μ and is finite.

    Remark. 

    The set S(To) of μ-terms is the set of input terms to derivations, given by applying a semantic function symbol to an OL term.

    Remark. 

    F and G contain additional function symbols do not represent semantic functions, are not inputs to any rules in RΦ, but can take arguments from TO, S(To), and Cm.

    Remark. 

    The set Tm of meta-linguistic terms of ΣM is the closure of Am∪To under Σm′∪S∪F∪G.

    Definition. Complex indirect constant μ-systems (§ 8.3.4) [pagin2021-CIC]

    A complex indirect constant μ-system Φ must satisfy the following.

    1. RΦ is finite.
    2. For any rule, the rewrite variables on the rhs must be a subset of those on the left.
    3. Rewrite variables v1,v2,... take all and only object language grammatical terms as instances.
    4. Rewrite variables y1,y2,... take all and only expressions in Cm as instances.
    5. Every atomic rule r∈RΦ is of the form μi(t)→e where μi∈S, t∈AO and e is a simple or complex expression in Cm.
    6. For every pair ⟨μi∈S,t∈Ao⟩ there is an atomic rule.
    7. Every direct complex rule r has the form μi(α(v1,...,vn))→K(μk1(v1),...,μkn(vn))⇐Gr(α(v1,...,vn)) where Gr corresponds to grammaticality.
    8. Every indirect complex rule has the form μi(α(v1,...,vn))→f(μk1(v1),...,μkn(vn),v1,...,vn)⇐Gr(α(v1,...,vn)) where v1,...,vn are optional and f∈F.
    9. For every pair ⟨μi∈S,α∈Σo′, there is a unique complex (indirect or direct) rule.
    10. Every indirect ground rule is of the F-form f(y1,...,yn,...,tn)→K′(f′(y1,...,yn)) or the G-form g(e1,...,en)→K(e1,...,en) where f,f′∈F, g∈G, K,K′ are operators over Σm′, e1,...,en∈Am and t1,...,tj∈Ao, and at most one of the primed operators is null.
    11. Every indirect recurisve rule in RΦ has an F-form f(y1,...,yn,σ(v1,...,vn))→K(f(y1,...,yn,v1)...,f(y1,...,yn,vn)) or G-form g(K(y1,...,yn))→K′(g′(y1,...,yn)) where f∈F, g,g′∈G, K,K′ are operators over Σm′, σ∈ΣO′, and at most one of the primed operators is null.

    Proposition.  [pagin2021-cic-terminate]

    Complex indirect constant systems are convergent (§ 8.3.4).

    Corollary.  [pagin2021-mdl]

    Given a complex indirect constant μ-system, for any term t, there is some minimum derivation length to a unique normal form.

    Proposition.  [pagin2021-general]

    Let Φ be any complex indirect constant μ-system satisfying the following.

    1. For every n⩾1, there are object-language atoms a1,...an∈Ao such that for every 1⩽k⩽n, where t1=α1 and tk+1=δ(αk+1,tk), for some canonical expression e∈Cm, μ(tk)→Φ+e, and tk∈To.
    2. The complex rule for μ,δ is μ(δ(v1,v2))→f(μ(v1),μ(v2),v2)⇐Gr(d(v1,v2)).
    3. There are rules f(y1,y2,δ(v1,v2))→K(f(y1,y2,v1),f(y1,y2,v2)) and f(y1,y2,α)→Kα(y1,y2) for each α∈Ao.

    Then Φ is intractable.

    Lemma. 

    Fix some k⩾1 and α1,...,αk. Define F(t):=f(μ(αk+1,μ(tk),t′)).

    Moreover, define l(t) as the number of atomic leaves of t.

    For every object-language subterm t of tk, T(F(t))⩾l(t)·T(μ(tk)).

    Proof. 

    By structural induction on t.

    If t=α∈AO, F(α) has subterm μ(tk), which must be reduced to eliminate m to obtain a canonical form. Moreover, there is only one atomic leaf. So T(F(a))⩾T(μ(tk))=1·T(μ(tk)).

    Suppose t=δ(t1,t2). Normalisation requires elimination of the root f of F(t). Since the third argument has head δ, only f(y1,y2,δ(v1,v2))→K(f(y1,y2,v1),f(y1,y2,v2)) will do so. Every derivation (minimum-length or otherwise) will have to apply that rule at some point. Without loss of generality, apply it at the beginning. Then F(t)→K(F(t1),F(t2)). Note K is terminal by definition of complex indirect constant μ-systems. So T(F(t))=1+T(F(t1))+T(F(t2))⩾l(t1)·T(μ(tk))+l(t2)·T(μ(tk))=l(t)·T(μ(tk)).

    Proof.. 

    Now consider a minimum-length derivation of μ(tk+1). There is some minimum-length derivation that begins μ(tk+1)→F(tk) whence T(μ(tk+1))=1+T(F(tk))⩾k·T(μ(tk)) whence T(μ(tn))⩾(n−1)!.

    Backlinks

      Definition. Compositionality, computability, and complexity › Term rewrite systems (§ 6.1) › Conditional term rewrite systems (§ 6.1) [pagin2021-ctrs]

      In a conditional term rewrite system ΣΦ,RΦ, the reductions are conditioned over some conditions C1,...,Cn.

      Definition. Compositionality, computability, and complexity › Term rewrite systems (§ 6.1) › Many-sorted term rewrite systems (§ 6.1) [pagin2021-many-sorted-trs]

      In a many-sorted term rewrite system, TPsi is partitioned into subsets corresponding to sorts, and argument places for operators have sort restrictions; complex terms whose subterms satisfy the sort restrictions are well-sorted (corresponding to grammaticality).