Pagin, ‘Compositionality, computability, and complexity’

0.1. Definition. (Grammatical term algebra (§ 2.1))   A grammatical term algebra GTA𝐿 of a language 𝐿 is a partial algebra ⟨GT𝐿,AT𝐿,Σ𝐿⟩, where—

  1. GT𝐿 is the set of grammatical terms for 𝐿,
  2. AT𝐿 is a finite set of atomic (grammatical) terms for 𝐿, and
  3. Σ𝐿 is a finite set of syntactic operations for 𝐿. GT𝐿 is the closure of AT𝐿 under Σ𝐿.
0.2. Definition. (Meaning operations (§ 2.2))   A meaning operation 𝑟 over a domain of meanings 𝑀 is some function 𝑀𝑛→𝑀.
0.3. Definition. (Semantic functions (§ 2.2))   Where GTA𝐿 is a grammatical term algebra and 𝑀 is a domain of meanings, any 𝜇:GT𝐿→𝑀 is a semantic function.

0.4. Definition. (Standard compositionality (§ 2.2))   Given a grammatical term algebra GTA𝐿 and domain 𝑀 of meanings, a semantic function 𝜇:GT𝐿→𝑀 is standard compositional iff for every 𝑛-ary operation 𝜎∈Σ𝐿 there is a meaning operation 𝑟𝜎:𝑀𝑛→𝑀 such that for any 𝑡1,…,𝑡𝑛∈Dom𝜎⊆GT𝐿,

𝜇(𝜎(𝑡1,…,𝑡𝑛))=𝑟𝜎(𝜇(𝑡1),…,𝜇(𝑡𝑛)).

0.5. Definition. (General compositionality (§ 2.3))   A semantic system 𝑆 is general compositional iff for every 𝑛-ary operation 𝜎∈Σ𝐿 and every member 𝜇𝑖∈𝑆′ there is a meaning operation 𝑀𝑛→𝑀 such that for any grammatical terms 𝑡1,…,𝑡𝑛∈Dom𝜎

𝜇𝑖(𝜎(𝑡1,…,𝑡𝑛))=𝑟𝜎,𝑖(𝜇𝑗1(𝑡1),…,𝜇𝑗𝑛(𝑡𝑛)),

where for 1⩽𝑘⩽𝑛

𝜇𝑗𝑘=Φ𝑆(𝜇𝑖,𝜎,𝑘).

0.6. Definition. (Meaning algebras (§ 3))   A meaning algebra over a set of meanings 𝑀 is a triple MA𝑀=⟨𝑀,𝐵𝑀,𝑅𝑀⟩, where—

  1. 𝐵𝑀 is a finite set of basic meanings,
  2. 𝑅𝑀 is a finite set of elementary meaning operations,
  3. 𝑀 closes 𝐵𝑀 under 𝑅𝑀, and
  4. for all 𝛿,𝛿′∈𝑅𝑀 and 𝑥1,…𝑥𝑛,𝑦1,…,𝑦𝑚,

    𝛿(𝑥1,…,𝑥𝑛)∉𝐵𝑀

    and, if

    𝛿(𝑥1,…,𝑥𝑛)=𝛿′(𝑦1,…,𝑦𝑚)

    then 𝛿=𝛿′, 𝑚=𝑛, and 𝑥𝑖=𝑦𝑖 for 1⩽𝑖⩽𝑛.

0.7. Definition. (Semantic systems (§ 3))   Given a grammatical term algebra GTA𝐿 and domain 𝑀 of meanings, a semantic system 𝑆 is a triple ⟨𝑆′,𝜇𝑆,Φ𝑆⟩ where—

  1. 𝑆′ is a finite set of semantic functions 𝜇𝑗:GT𝐿→𝑀, 𝜇𝑆∈𝑆, and
  2. Φ𝑆:𝑆′×Σ𝐿×𝑁→𝑆′ is a partial selection function.

Given some semantic function 𝜇𝑗 and a syntactic operation 𝜎, Φ𝑆 then gives another semantic function 𝜇𝑘 for each 𝑛th-position term.

Finally, 𝑆(𝑡)=𝜇𝑆(𝑡).

0.8. Definition. (Semantic algebras (§ 3))   A semantic algebra over a language 𝐿 and domain 𝑀 of meanings is a triple

SALM=⟨⟨GT𝐿,𝑀⟩,⟨AT𝐿,𝐵𝑀⟩,⟨Σ𝐿,𝑅𝑀⟩⟩

where—

  1. ⟨GT𝐿,AT𝐿,Σ𝐿⟩ is a grammatical term algebra for 𝐿, and
  2. ⟨𝑀,𝐵𝑀,𝑅𝑀⟩ is a meaning algebra for 𝑀.
0.9. Definition. (Size (§ 5))   The size of a term is the number of atoms and operators contained within it.
0.10. Definition. (Input terms (§ 5))   The input terms of a rewriting system are of the form ‘𝜇(𝑡)’ where 𝑡 is a syntactic term.

0.11. Definition. (Input complexity (§ 5))   Let 𝑠 be a normal term.

The term complexity Ct𝑅(𝑠) of 𝑠 relative to 𝑅 is the length of the shortest derivation from some input term 𝜇(𝑡) to 𝑠.

The input complexity 𝐶𝑅𝑖(𝑘) is the maximal Ct𝑅(𝑠) where 𝑠 has size 𝑘.

0.12. Definition. (Term rewrite systems (§ 6.1))   A term rewrite system (TRS) Φ is a pair ⟨ΣΦ,𝑅Φ⟩ where—

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

We will write 𝑡1→Φ𝑡2 (omitting the subscript where context makes it obvious) when the application of some rule 𝑟∈𝑅Φ yields the contractum 𝑡2.

A sequence of applications 𝑡1→𝑡2→…→𝑡𝑛 is a derivation. We write 𝑡1→Φ+𝑡𝑛 where →Φ+ is the transitive closure of →.

0.13. Definition. (Conditional term rewrite systems (§ 6.1))   In a conditional term rewrite system ΣΦ,𝑅Φ, the reductions are conditioned over some conditions 𝐶1,…,𝐶𝑛.
0.14. Definition. (Many-sorted term rewrite systems (§ 6.1))   In a many-sorted term rewrite system, 𝑇Ψ 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).
0.15. Definition. (Normal form (§ 6.1))   A term that cannot be reduced further is in normal form.
0.16. Definition. (Termination (§ 6.1))   If every derivation leads to a term in normal form, a system terminates.
0.17. Definition. (Confluence (§ 6.1))   Φ is confluent iff, for all terms 𝑡1,𝑡2,𝑡3, whenever 𝑡1→Φ+𝑡2 and 𝑡1→Φ+𝑡3, there is some 𝑡4 such that 𝑡2→Φ+𝑡4 and 𝑡3→Φ+𝑡4.
0.18. Definition. (Convergence (§ 6.1))   A confluent system that terminates is convergent.

0.19. Definition. (#{\mu}-systems (§ 6.1))   A 𝜇-system is a pair Φ=⟨ΣΦ,𝑅Φ⟩ where—

  1. Σ=⟨Σ𝑜,Σ𝑚⟩ (an object- and meta-language signature),
  2. Σ𝑜=⟨𝐴𝑜,Σ′𝑜⟩ where 𝐴𝑜 is a set of atomic terms and Σ′ is a set of 𝑛-ary syntactic operators, so that the closure 𝑇𝑜 of 𝐴𝑂 under Σ′ yields the grammatical term algebra ⟨𝑇𝑂,𝐴𝑂,Σ′𝑂⟩ of OL,
  3. Σ𝑚=⟨𝐴𝑚,Σ′𝑚,𝑆,𝐹,𝐺⟩ where—
  4. 𝐴𝑚 is a nonempty set of atomic meta-language expressions,
  5. Σ′𝑚 is a nonempty set of meta-language syntactic operators,
  6. 𝑆 is a nonempty set of elementary meta-language function symbols,
  7. 𝐹 is a possibly empty set of meta-language recursive function symbols over object language terms, and
  8. 𝐺 is a possibly empty set of meta-language recursive function symbols over meta-language terms.
0.20. Remark.   The canonical expressions of ML, 𝐶𝑚, close 𝐴𝑚 under Σ′𝑚, canonically express meanings, do not contain any 𝜇 operators or 𝐹/𝐺 functors, and rewrite derivations terminate with them.
0.21. Remark.   The set 𝑆 of the semantic vocabulary of Φ contains at least the semantic function symbol 𝜇 and is finite.
0.22. Remark.   The set 𝑆(𝑇𝑜) of 𝜇-terms is the set of input terms to derivations, given by applying a semantic function symbol to an OL term.
0.23. Remark.   𝐹 and 𝐺 contain additional function symbols do not represent semantic functions, are not inputs to any rules in 𝑅Φ, but can take arguments from 𝑇𝑂, 𝑆(𝑇𝑜), and 𝐶𝑚.
0.24. Remark.   The set 𝑇𝑚 of meta-linguistic terms of Σ𝑀 is the closure of 𝐴𝑚∪𝑇𝑜 under Σ′𝑚∪𝑆∪𝐹∪𝐺.

0.25. Definition. (Complex indirect constant #{\mu}-systems (§ 8.3.4))   A complex indirect constant 𝜇-system Φ must satisfy the following.

  1. 𝑅Φ is finite.
  2. For any rule, the rewrite variables on the rhs must be a subset of those on the left.
  3. Rewrite variables 𝑣1,𝑣2,… take all and only object language grammatical terms as instances.
  4. Rewrite variables 𝑦1,𝑦2,… take all and only expressions in 𝐶𝑚 as instances.
  5. Every atomic rule 𝑟∈𝑅Φ is of the form

    𝜇𝑖(𝑡)→𝑒

    where 𝜇𝑖∈𝑆, 𝑡∈𝐴𝑂 and 𝑒 is a simple or complex expression in 𝐶𝑚.

  6. For every pair ⟨𝜇𝑖∈𝑆,𝑡∈𝐴𝑜⟩ there is an atomic rule.
  7. Every direct complex rule 𝑟 has the form

    𝜇𝑖(𝛼(𝑣1,…,𝑣𝑛))→𝐾(𝜇𝑘1(𝑣1),…,𝜇𝑘𝑛(𝑣𝑛))⇐Gr(𝛼(𝑣1,…,𝑣𝑛))

    where Gr corresponds to grammaticality.

  8. Every indirect complex rule has the form

    𝜇𝑖(𝛼(𝑣1,…,𝑣𝑛))→𝑓(𝜇𝑘1(𝑣1),…,𝜇𝑘𝑛(𝑣𝑛),𝑣1,…,𝑣𝑛)⇐Gr(𝛼(𝑣1,…,𝑣𝑛))

    where 𝑣1,…,𝑣𝑛 are optional and 𝑓∈𝐹.

  9. For every pair ⟨𝜇𝑖∈𝑆,𝛼∈Σ′𝑜, there is a unique complex (indirect or direct) rule.
  10. Every indirect ground rule is of the 𝐹-form

    𝑓(𝑦1,…,𝑦𝑛,…,𝑡𝑛)→𝐾′(𝑓′(𝑦1,…,𝑦𝑛))

    or the 𝐺-form

    𝑔(𝑒1,…,𝑒𝑛)→𝐾(𝑒1,…,𝑒𝑛)

    where 𝑓,𝑓′∈𝐹, 𝑔∈𝐺, 𝐾,𝐾′ are operators over Σ′𝑚, 𝑒1,…,𝑒𝑛∈𝐴𝑚 and 𝑡1,…,𝑡𝑗∈𝐴𝑜, and at most one of the primed operators is null.

  11. Every indirect recurisve rule in 𝑅Φ has an 𝐹-form

    𝑓(𝑦1,…,𝑦𝑛,𝜎(𝑣1,…,𝑣𝑛))→𝐾(𝑓(𝑦1,…,𝑦𝑛,𝑣1)…,𝑓(𝑦1,…,𝑦𝑛,𝑣𝑛))

    or 𝐺-form

    𝑔(𝐾(𝑦1,…,𝑦𝑛))→𝐾′(𝑔′(𝑦1,…,𝑦𝑛))

    where 𝑓∈𝐹, 𝑔,𝑔′∈𝐺, 𝐾,𝐾′ are operators over Σ′𝑚, 𝜎∈Σ′𝑂, and at most one of the primed operators is null.

0.26. Proposition.   Complex indirect constant systems are convergent (§ 8.3.4).
0.1. Corollary.   Given a complex indirect constant 𝜇-system, for any term 𝑡, there is some minimum derivation length to a unique normal form.

0.27. Proposition.   Let Φ be any complex indirect constant 𝜇-system satisfying the following.

  1. For every 𝑛⩾1, there are object-language atoms 𝑎1,…𝑎𝑛∈𝐴𝑜 such that for every 1⩽𝑘⩽𝑛, where 𝑡1=𝛼1 and 𝑡𝑘+1=𝛿(𝛼𝑘+1,𝑡𝑘), for some canonical expression 𝑒∈𝐶𝑚, 𝜇(𝑡𝑘)→Φ+𝑒, and 𝑡𝑘∈𝑇𝑜.
  2. The complex rule for 𝜇,𝛿 is

    𝜇(𝛿(𝑣1,𝑣2))→𝑓(𝜇(𝑣1),𝜇(𝑣2),𝑣2)⇐Gr(𝑑(𝑣1,𝑣2)).
  3. There are rules

    𝑓(𝑦1,𝑦2,𝛿(𝑣1,𝑣2))→𝐾(𝑓(𝑦1,𝑦2,𝑣1),𝑓(𝑦1,𝑦2,𝑣2))

    and

    𝑓(𝑦1,𝑦2,𝛼)→𝐾𝛼(𝑦1,𝑦2)

    for each 𝛼∈𝐴𝑜.

Then Φ is intractable.

0.28. Lemma.   Fix some 𝑘⩾1 and 𝛼1,…,𝛼𝑘. Define

𝐹(𝑡)≔𝑓(𝜇(𝛼𝑘+1,𝜇(𝑡𝑘),𝑡′)).

Moreover, define 𝑙(𝑡) as the number of atomic leaves of 𝑡.

For every object-language subterm 𝑡 of 𝑡𝑘,

𝑇(𝐹(𝑡))⩾𝑙(𝑡)⋅𝑇(𝜇(𝑡𝑘)).

Proof. By structural induction on 𝑡.

If 𝑡=𝛼∈𝐴𝑂, 𝐹(𝛼) has subterm 𝜇(𝑡𝑘), which must be reduced to eliminate 𝑚 to obtain a canonical form. Moreover, there is only one atomic leaf. So

𝑇(𝐹(𝑎))⩾𝑇(𝜇(𝑡𝑘))=1⋅𝑇(𝜇(𝑡𝑘)).

Suppose 𝑡=𝛿(𝑡1,𝑡2). Normalisation requires elimination of the root 𝑓 of 𝐹(𝑡). Since the third argument has head 𝛿, only

𝑓(𝑦1,𝑦2,𝛿(𝑣1,𝑣2))→𝐾(𝑓(𝑦1,𝑦2,𝑣1),𝑓(𝑦1,𝑦2,𝑣2))

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

𝐹(𝑡)→𝐾(𝐹(𝑡1),𝐹(𝑡2)).

Note 𝐾 is terminal by definition of complex indirect constant 𝜇-systems. So

𝑇(𝐹(𝑡))=1+𝑇(𝐹(𝑡1))+𝑇(𝐹(𝑡2))⩾𝑙(𝑡1)⋅𝑇(𝜇(𝑡𝑘))+𝑙(𝑡2)⋅𝑇(𝜇(𝑡𝑘))=𝑙(𝑡)⋅𝑇(𝜇(𝑡𝑘)).

Proof. Now consider a minimum-length derivation of 𝜇(𝑡𝑘+1). There is some minimum-length derivation that begins

𝜇(𝑡𝑘+1)→𝐹(𝑡𝑘)

whence

𝑇(𝜇(𝑡𝑘+1))=1+𝑇(𝐹(𝑡𝑘))⩾𝑘⋅𝑇(𝜇(𝑡𝑘))

whence 𝑇(𝜇(𝑡𝑛))⩾(𝑛−1)!.⁠□

References

Pagin, Peter, ‘Compositionality, computability, and complexity’, The Review of Symbolic Logic 14.3 (2021), pp 551–591.