Lit / Ro88

Ro88: William C. Rounds. 1988. LFP: A Logic for linguistic descriptions and an analysis of its complexity

  • LitD:Ro88.pdf
  • Computational Linguistics, Volume 14, Number 4, December 1988

CLFP concatenation grammar (Concatenation, first order logic plus LFP (Least-Fixed-Point) ) Grammatik beschreibt genau die in exponentieller Zeit erkennbaren Sprachen. ILFP - analog aber mit Indexen (Substrings) beschreibt genau die in polinomialer Zeit erkennbaren Sprachen.

Algorithmus ist der gleiche, aber einmal werden Substrings zwischengespeichert, das andere mal binär Codiert Indizes.

2 CLFP GRAMMARS BASED ON CONCATENATION THEORY

We present a standard version of the first-order theory of concatenation, augmented with the least-fixed-point (LFP) operator.

CLFP

  • Ivar: Set of individual variables über Strings
  • Σ: set of terminal symbols (Konstants)
  • Terms are built from variables and constants using the binary operation of concatenation
  • Λ: empty String
  • Pvar;: Predicate Variables mit arity ar(P)
  • CLFP Formulas
    1. P(x1, ... xar(P)) mit P ∈ Pvar und xi ∈ Ivar (??? oder Terms? ist irrelevant mittels .... and xi = term )
    2. t = u: equality of terms
    3. ∃xφ und ∀xφ: Quantification mit φ ∈ CLFP
    4. usual boolean combinators of formulas
    5. μSΦ: the least fixed point of Φ for S with
      • S ∈ R ⊆ Pvar
      • Φ: R → Powerset(Ivar) × CLFP with ar(Q) = |X| for Φ(Q) = (X,φ) (??? Sequence not powerset?)
      • Φ is a recursion scheme iff ∀ P,Q ∈ R: P occurs only positively in Q (i.e. after even number of ^ )
      • Φ is not formulated explicitly in CLFP, but deduced from the normal definitions of the P ∈ R

semantics

  • A: {α : Ivar → Σ*}: assignment der Variabeln
  • ρ : R → Relation über Σ* with ar(S) = ar(ρ(S))
  • M[[φ]]ρ ⊆ A: set of assignments for which φ is true
    • only difficulty are recursion schemes: there we use induction Φ0: empty relations, Φi+1 evaluated from Φi
  • M[[φ]]ρn: bounded to strings of length <= n

Theorem1. A language (unary predicate) is boundedly definable in CLFP iff it is in EXPTIME .

EXPTIME and CLFP

  • ATM: alternating touring machine
    • states: existential, universal, negating, accepting
    • multiple work tapes - one for each bound variable

Proof of theorem1 by constructing ATM accepting language of φ. respectively reformulatin ATM as formula φ and using EXPTIME = ASPACE( n )

4 ILFP : GRAMMARS WITH INTEGER INDEXING

statt Strings zwischenspeichern nur Indexe in zu analysierenden String

ILFP durch abändern von CLFP, für Input von Länge n (Positionen 0..n-1)

  • Ivar und Terms sind integer 0 .. n-1, + - * und div 2 (alles mod n) - Konstanten 0, 1 last=n-1. keine Konkatinationen sondern trennen durch Substring Indexe
  • a(i) ist Prädikat char at pos i == a
  • Rekursionsschema wie gehabt

Theorem 2. A language is ILFP-definable iff it is in PTIME.

Beweis gleiche Konstruktion wie für Theorem 1 und We also know that PTIME = ASPACE( Iog n) ==> Indexe brauchen nur log2 n bits