From finite semantics to regular languages(and beyond) in second-order linear logicNguyễn Lê Thành Dũng (a.k.a. Tito) — nltd@nguyentito.eu
Laboratoire d’informatique de Paris Nord (LIPN), Université Paris 13
joint work with Thomas Seiller (CNRS, LIPN)
ELICA project final meeting, Paris, October 11th, 2018

1/20

Implicit complexity with proofs-as-programs
Curry-Howard approach to implicit complexity:
1. Define logic / programming language
2. Bound evaluation complexity (soundness)
3. Show language expressivity (extensional completeness)
4. Result: set of expressible functions = some complexity class
Step 1 requires creativity. Examples from linear logic:
LLL ⇝ polytime (Girard), SBAL ⇝ logspace (Schöpp)…

2/20

Implicit complexity with proofs-as-programs
Curry-Howard approach to implicit complexity:
1. Define logic / programming language
2. Bound evaluation complexity (soundness)
3. Show language expressivity (extensional completeness)
4. Result: set of expressible functions = some complexity class
Step 1 requires creativity. Examples from linear logic:
LLL ⇝ polytime (Girard), SBAL ⇝ logspace (Schöpp)…
This talk: instead, ask (2)–(4) for well-known systems:• simply typed λ-calculus (STλ)• recall old methods and results• and later Elementary Linear Logic (ELL)• new results inspired by STλ techniques…or rather, (naturally) restricted situations within STλ/ELL.

2/20

Simply-typed λ-calculus and implicit complexity?
Recall k-EXPTIME∪= DTIME(tower of exponentials of height k),
ELEMENTARY =k-EXPTIME.
k∈N

Claim: STλ characterizes ELEMENTARY.
Parameter controlling complexity: functionality orderord(α → β) = max(ord(α) + 1, ord(β))• Soundness: ∀k ∈ N ∃f(k) ∈ N s.t. normalization ofλ-terms with order ≤ k subterms is in f(k)-EXPTIME• Extensional completeness: naive attempt fails
3/20

Church encodings of inputs in STλChurch (or Böhm–Berarducci) encodings:• For w ∈ {0, 1}∗ , w : Str[A] for any simple type A (meta-∀)• Str[A] = (A → A) → (A → A) → (A → A)
• w = λf0 . λf1 . λx. fw[0] (. . . (fw[n−1] x) . . .)• Bool = o → o → o (o base type)
Choose a simple type A, and a term t : Str[A] → Bool−→ defines language L(t) = {w ∈ {0, 1}∗ | t w →∗β true}.
Not all ELEMENTARY languages possible… but then what?

4/20

Church encodings of inputs in STλChurch (or Böhm–Berarducci) encodings:• For w ∈ {0, 1}∗ , w : Str[A] for any simple type A (meta-∀)• Str[A] = (A → A) → (A → A) → (A → A)
• w = λf0 . λf1 . λx. fw[0] (. . . (fw[n−1] x) . . .)• Bool = o → o → o (o base type)
Choose a simple type A, and a term t : Str[A] → Bool−→ defines language L(t) = {w ∈ {0, 1}∗ | t w →∗β true}.
Not all ELEMENTARY languages possible… but then what?
Theorem (Hillebrand & Kanellakis, LICS’96)
The languages decided by STλ-terms of type Str[A] → Bool areexactly the regular languages.
4/20

Regular languages in STλTheorem (Hillebrand & Kanellakis, LICS’96)
For any type A and any STλ-term t : Str[A] → Bool, the language
L(t) = {w ∈ {0, 1}∗ | t w →∗β true} is regular.
Part 1 of proof.
Fix type A. Any denotational semantics J−K quotients words:w ∈ {0, 1}∗ ⇝ w : Str[A] ⇝ JwKStr[A] ∈ JStr[A]KWhen J−K non-trivial (JtrueK ̸= JfalseK), JwKStr[A] determines
behavior of w w.r.t. all Str[A] → Bool terms:w ∈ L(t) ⇐⇒ t w →∗β true ⇐⇒ Jt wK = JtK(JwK) = JtrueK
Goal: to decide L(t), compute w 7→ JwK in some model of STλ.
5/20

Regular languages in STλTheorem (Hillebrand & Kanellakis, LICS’96)
For any type A and any STλ-term t : Str[A] → Bool, the language
L(t) = {w ∈ {0, 1}∗ | t w →∗β true} is regular.
Part 2 of proof.
We use J−K : STλ → FinSet to build a DFA with states
Q = JStr[A]K, acceptation as JtK(−) = JtrueK.

JεK

0q y0

1q y01

1q y011...

()w ∈ L(t) ⇐⇒ JtK JwKStr[A] = JtrueK ⇐⇒ w accepted−→ semantic evaluation argument.
5/20

Regular languages in STλTheorem (Hillebrand & Kanellakis, LICS’96)
For any type A and any STλ-term t : Str[A] → Bool, the language
L(t) = {w ∈ {0, 1}∗ | t w →∗β true} is regular.
Part 2 of proof.
We use J−K : STλ → FinSet to build a DFA with states
Q = JStr[A]K, acceptation as JtK(−) = JtrueK.
33(|Q| < ∞, e.g. 22 when A = Bool)
JεK

0q y0

1q y01

1q y011...

()w ∈ L(t) ⇐⇒ JtK JwKStr[A] = JtrueK ⇐⇒ w accepted−→ semantic evaluation argument.
5/20

Moral of the story
Finite denotational semantics have complexity consequences.
• Analogous results for tree automata, and for propositional
linear logic (using your favorite finite model)• Another application to STλ at fixed order:
Theorem (Terui, RTA’12)
Normalizing an STλ-term of type Bool w/ order ≤ r subterms is• k-EXPTIME-complete for r = 2k + 2• k-EXPSPACE-complete for r = 2k + 3
Proof of membership in k-EXPTIME / k-EXPSPACE.
β-reduce to halve order, then evaluate in LL Scott model.
6/20

Extensional completeness for STλNeed to change input representation!
Hillebrand, Kanellakis & Mairson, motivated by databasequeries, encode finite relational (1st-order) structures as inputs−→ completeness for ELEMENTARY.
• We’ll come back to this later• “β-convertibility of STλ terms ∈/ ELEMENTARY”(Statman 1979) can be recovered from this• Refined by H&K: characterization of k-EXPTIME /k-EXPSPACE in STλ+constants+equality at fixed order• Also using semantic evaluation for soundness!

7/20

Regular languages in
Elementary Linear Logic

Elementary Linear Logic (ELL)
ELL = Multiplicative-Additive Linear Logic (MALL) + ?/! rules:⊢ Γ, ?A, ?A⊢ Γ, ?A⊢Γ
⊢ Γ, ?A⊢ A1 , . . . , An , B⊢?A1 , . . . , ?An , !B!-intro: promotion and dereliction must come together.
−→ enforces stratification by !-depth(subproofs cannot change depth during cut-elimination)
Representable functions in 2nd-order ELL = ELEMENTARY:• Soundness: normalization in f(depth)-EXPTIME• depth in ELL ≃ order in STλ• Extensional completeness: Church encoding works• thanks to (impredicative) polymorphism!
8/20

Complexity in second-order ELL (1)Data types:• Bool = 1 ⊕ 1• Str = ∀X. !(X ⊸ X) ⊸ !(X ⊸ X) ⊸ !(X ⊸ X)
Extensional completeness: all languages L ∈ ELEMENTARY
expressible by ELL proofs of !Str ⊸!k Bool (k depends on L).
Soundness (reformulated):
proofs of !k Bool can be normalized in f(k)-EXPTIME.
Question: what do we get for a fixed depth k?

9/20

Complexity in second-order ELL (2)Depth k = 2 case, in a variant of ELL:
Theorem (Baillot, APLAS’11)
The proofs of !Str ⊸ !!Bool in 2nd order elementary affine logic
with recursive types decide exactly the languages in P.

10/20

Complexity in second-order ELL (2)Depth k = 2 case, in a variant of ELL:
Theorem (Baillot, APLAS’11)
The proofs of !Str ⊸ !!Bool in 2nd order elementary affine logic
with recursive types decide exactly the languages in P.
Recursive types are crucial for the above, as we show:
Theorem
The proofs of !Str ⊸ !!Bool in 2nd order ELL decide exactly theregular languages.
Proof idea.
Adapt Hillebrand & Kanellakis’s STλ proof. Requires
non-trivial finite semantics for 2nd order MALL (MALL2).
10/20

Finite semantics for MALL2
Choice of semantics: syntax/(observational equivalence).
Definition (Eqv. for propositional observations)
Let A be a MALL2 formula and π, π ′ : A. Define π ∼A π ′ as:∀B MALL0, ∀ρ : (A ⊢ B), cut(π, ρ) ≡ cut(π ′ , ρ)
• MALL0 = propositional MALL
• ≡ is usual proof equivalence on MALL0 (think =βη )Theorem
For any MALL2 formula A, there are finitely many classes for ∼A .
Corollary
There exists a non-trivial finite semantics for MALL2.
New result of independent interest, cf. Pistone’s talk 2 days ago.

11/20

Semantic evaluation in ELL, in a nutshell
Let π : !Str ⊸ !!Bool. There existsπb : Str[A1 ] ⊸ . . . ⊸ Str[An ] ⊸ !Boolsuch that ∀w. π(!w) = !bπ (w[A1 ], . . . , w[An ]).

(Str = ∀X. Str[X])Thanks to stratification, w.l.o.g. A1 , . . . , An ∈ MALL2.
Using finite MALL2 semantics J−K, w[A] induces map∥w∥A : JA ⊸ AK × JA ⊸ AK → JA ⊸ AK
such that w[A](!f1 , !f2 ) = !g =⇒ ∥w∥A (Jf1 K , Jf2 K) = JgK.
• Church encoding −→ ∥w∥A computable by automatonb(w[A1 ], . . . , w[An ])• (∥w∥A1 , . . . , ∥w∥An ) determine π
and therefore π(!w)
12/20

What about higher depths?
We solved depth k = 2 case for ELL.
(First characterization of regular languages in a type systemwith impredicative quantification?)
When k > 2 :Theorem (Baillot, APLAS’11)
The proofs of !Str ⊸ !k Bool in EAL+rectypes decide exactly thelanguages in (k − 2)-EXPTIME.
• For ELL without recursive types, we get a class between(k − 3)-EXPTIME and (k − 2)-EXPTIME… which one exactly?
• Semantics probably has a role to play in the answer
13/20

Inputs as finite models:
towards logarithmic space in ELL?

A bit of descriptive complexity

Data represented as (totally ordered) finite first-order structures(a.k.a. finite models), over a signature of relation symbols.
ExampleSignature for binary strings: ⟨≤, S⟩.
Finite models are (D, ≤D , SD ), |D| < ∞. SD (d) = “dth bit is 1”.
Descriptive complexity: characterize a complexity class C as set ofqueries written in some logic LC , i.e. “is this LC formula true inthis finite model?”. For instance:
Theorem (Fagin 1974)
Queries in existential second-order logic = NP.

14/20

Finite models in STλ and extensional completenessWith type d of elements (equipped with Eq : d → d → Bool),• Represent k-ary relations as lists of k-tuples
Relk [d, A] = (dk → A → A) → A → A(in the spirit of database theory: relation = set of records)• Provide list of all domain elements (List[d, A] = Rel1 [d, A])
Theorem (Hillebrand, Kanellakis & Mairson, LICS’93)
Terms t : List[d, A] → Relk1 [d, A1 ] → . . . → Relkm [d, Am ] → Boolin STλ compute exactly ELEMENTARY queries over finite models.
To feed input, instantiate d = on → o (n = domain size).
Program has “∀d ∃A”, input has “∃d ∀A”. Size of semantics
depends on input, breaking earlier expressivity upper bound.
15/20

Finite models in ELL
We transpose this idea to second-order ELL:
• We use Relk [D] = D⊗k ⊸ Bool,List[D] = ∀X. !(D ⊸ X ⊸ X) ⊸ !(X ⊸ X)
• Allow non-linear use of D:
Cont[D] = D ⊸ D ⊗ D, Wk[D] = D ⊸ 1
Inpr = ∃D. !List[D] ⊗n⊗!r Relki [D]⊗ !r Cont[D]⊗ !r Wk[D]i=1(choose r to satisfy stratification constraint)• For size n domain, witness D = 1 ⊕ . . . (n times) . . . ⊕ 1(positive, therefore duplicable)
16/20

Towards logarithmic space in ELL? (1)Theorem (Immerman 1983)
Queries in first-order logic with deterministic transitive closure =logarithmic space (L) queries.
PropositionAll L queries on finite models for a given signature can be computedby an ELL proof of Inp2 ⊸ !!Bool.
Proof idea: compute transitive closure of a relation
R ⊆ Dk × Dk by iterating φR : P(Dk × Dk ) → P(Dk × Dk ).
Determinism of R ensures linearity: φR : Rel2k ⊸ Rel2k in ELL.
This is remarkable enough to hope for:Conjecture
Conversely, proofs of Inp2 ⊸ !!Bool only decide L queries.
17/20

Towards logarithmic space in ELL? (2)Conjecture
ELL proofs of the following type only decide L queries:()n⊗∃D. !List[D] ⊗!!Relki [D]⊗ !!Cont[D]⊗ !!Wk[D] ⊸ !!Booli=1

In predicative case (∀/∃ range over propositional formulae):• conjecture seems very likely• already non-trivial… (maybe Geometry of Interaction works?)• note that ext. completeness holds w/o impredicativity
In general case, I have no intuition or methods available
18/20

Conclusion and future work

Conclusion
We brought methods from the STλ tradition to 2nd order ELL,
showing that similar phenomena occur in both:• Church encodings of inputs restrict expressivity• Semantic evaluation can prove this (and lots of other stuff)• To overcome this, one can represent inputs as finite models
Lemma (or Theorem, if you care about semantics)
The quotient of MALL2 by propositional observations is finite.
Theorem (or Corollary)
Proofs of !Str ⊸ !!Bool in ELL decide regular languages.
Moral: geometry (e.g. stratification) and typing jointly control
complexity; semantics reflects the latter.
19/20

Open problems / future work
Logspace conjecture: what kind of techniques can solve this??
Classes characterized by higher fixed depths?
(For both !Str ⊸ !k Bool and Inpk ⊸ !k Bool…)
Related: complexity of normalizing a proof of !k Bool in ELL?
• k = 0: P-complete• k = 1: PSPACE-hard, in EXPTIME• k ≥ 2: (k − 1)-EXPTIME-hard, in k-EXPTIME(For EAL+rectypes, k-EXPTIME-complete by Baillot’s results.)
On MALL2 semantics: further investigations ongoing,
j.w.w. P. Pistone and L. Tortora de Falco.
20/20