Rachunek lambda, lato 2019-20

(1)

Rachunek lambda, lato 2019-20

Wykład 12

22 maja 2020

(2)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

Example: Peirce’s Law

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat). Indeed, there is no normal M with

x : (p → q) → p ` M : p

(3)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat).

Indeed, there is no normal M with x : (p → q) → p ` M : p

(4)

Classical (unnatural) deduction

¹

Γ, ¬σ ` ⊥

(Cheat) Γ ` σ

((p → q) → p) → p

is classically valid, but unprovable without rule (Cheat).

Indeed, there is no normal M with x : (p → q) → p ` M : p

(5)

Representing data types

I Natural numbers are generated by

I Constant0 : int;

I Successors : int → int.

They correspond to long normal forms of type ω = (0 → 0) → 0 → 0

I Words over {a, b} are generated by

I Constantε : word;

I Two successorsλλw (a · w ) andλλw (b · w ) of type word→ word.

They correspond to long normal forms of type word = (0 → 0) → (0 → 0) → 0 → 0

(6)

Representing data types

I Constant0 : int;

(7)

Representing data types

I Constant0 : int;

(8)

Representing data types

I Constant0 : int;

They correspond to long normal forms of type

(9)

Representing data types

I Binary trees are generated by

I Constantnil : tree;

I Constructorcons : tree → tree → tree.

They correspond to long normal forms of type tree = (0 → 0 → 0) → 0 → 0

Generalization:

Term algebras correspond to types of order two, i.e, of the form (0ⁿ¹ → 0) → · · · → (0ⁿ^k → 0) → 0

(10)

Representing data types

Generalization:

(11)

Representing data types

Generalization:

(12)

Representing data types

Types of order three and up define more complex structures.

For instance, long normal forms of type ((0 → 0) → 0) → 0 → 0 are as follows:

λF λx₀. F (λx₁. F (λx₂. F (λx₃F . . . λx_k. x_`) . . .)).

(13)

Type reducibility

Definition: Type τ is reducible to type σ iff there exists a closed term Φ : τ → σ such that the operator λλM:τ. ΦM is injective on closed terms, i.e.,

ΦM₁ =_βη ΦM₂ implies M₁ =_βη M₂ for closedM1, M2 : τ.

Examples:

I Typeω is reducible to type word usingΦ = λnfgx .nfx.

I Typesα → β → 0 and β → α → 0 are reducible to each other using Φ = λxyz. xzy.

I Typeword is reducible to type tree using Φ = λwcn.w (λx . cnx )(λx . cxn)(cnn).

(14)

Type reducibility

Examples:

(15)

Type reducibility

Examples:

(16)

Type reducibility

Examples:

(17)

Example

Encoding wordw = aab = a · a · b · ε as a tree,

corresponding toΦw = λcn.w (λx . cnx )(λx . cxn)(cnn).

c

n c

c n

(18)

A nice theorem

Theorem (R. Statman):

Every type over a single type constant0 is reducible to tree.

Idea dowodu

wg Thierry’ego Joly w kilku krokach.

(19)

Krok pierwszy

Lemat: Każdy typ nad 0 można zredukować do typu J = (0 → 0 → 0) → ((0 → 0) → 0) → 0.

Pomysł na dowód:

Kombinatory typu J są postaci λ@ λ∆. W, gdzie:

@ : 0 → 0 → 0, ∆ : (0 → 0) → 0 ` W : 0. Operatory @i ∆ mogą naśladować aplikację i abstrakcję.

(20)

Krok pierwszy

Pomysł na dowód:

@ : 0 → 0 → 0, ∆ : (0 → 0) → 0 ` W : 0.

Operatory @i ∆ mogą naśladować aplikację i abstrakcję.

(21)

Krok pierwszy

Pomysł na dowód:

@ : 0 → 0 → 0, ∆ : (0 → 0) → 0 ` W : 0.

Operatory @i ∆ mogą naśladować aplikację i abstrakcję.

(22)

Redukcja do typu J

Mając „stałe” @ : 0 → 0 → 0 i ∆ : (0 → 0) → 0, możemy zakodować dowolny term jako term typu0.

Na przykład term2 = λfx. f (fx) zakodujemy jako Dwa = ∆(λf⁰. ∆(λx⁰. @f (@fx )))

Bardziej sugestywna notacja:

— piszmyΛx zamiast ∆(λx oraz M · N zamiast @MN. Wtedy term Dwa napiszemy tak: Λf⁰Λx⁰. f · (f · x ) Opuszczamy szczegóły.

(23)

Redukcja do typu J

— piszmyΛx zamiast ∆(λx oraz M · N zamiast @MN. Wtedy term Dwa napiszemy tak: Λf⁰Λx⁰. f · (f · x ) Opuszczamy szczegóły.

(24)

Redukcja do typu J

— piszmyΛx zamiast ∆(λx oraz M · N zamiast @MN. Wtedy term Dwa napiszemy tak: Λf⁰Λx⁰. f · (f · x )

(25)

Redukcja do typu J

J = (0 → 0 → 0) → ((0 → 0) → 0) → 0.

Γ = {@ : 0 → 0 → 0, ∆ : (0 → 0) → 0}.

Dla dowolnegoτ, definiujemy termy Uτ i Vτ, takie że:

Γ ` U_τ : τ → 0 Γ ` V_τ : 0 → τ Indukcja: U0= V0= I,

U_ρ→σ = λf^ρ→σ. ∆(λx⁰U_σ(f (V_ρ(x )))) V_ρ→σ = λy⁰λz^ρ. V_σ(@y (U_ρz))

Redukcja typuτ doJ jest dana przez term λf^τλ@λ∆. U_τf. opuszczone

(26)

Γ = {@ : 0 → 0 → 0, ∆ : (0 → 0) → 0}.

Definiujemy termy U_τ : τ → 0, V_τ : 0 → τ Uρ→σ = λf^ρ→σ. ∆(λx⁰Uσ(f (Vρ(x )))) V_ρ→σ = λy⁰λz^ρ. V_σ(@y (U_ρz))

Sens tej definicji:

U_ρ→σ(f ): x : 0−→ ρ^V^ρ −→ σ^f −→ 0^U^σ

Vρ→σ(y ): z : ρ −→ 0^U^ρ −→ 0^@y −→ σ^V^σ

(27)

Krok drugi

Zredukowaliśmy dowolny typ do typu:

J = (0 → 0 → 0) → ((0 → 0) → 0) → 0 czyli do J = bool → ((0 → 0) → 0) → 0.

Teraz zredukujemy końcówkę((0 → 0) → 0) → 0 do typu word = (0 → 0) → (0 → 0) → 0 → 0. (Potem zredukujemy J do typu bool → word.)

(28)

Krok drugi

J = (0 → 0 → 0) → ((0 → 0) → 0) → 0 czyli do J = bool → ((0 → 0) → 0) → 0.

Teraz zredukujemy końcówkę((0 → 0) → 0) → 0 do typu word = (0 → 0) → (0 → 0) → 0 → 0.

(Potem zredukujemy J do typubool → word.)

(29)

Krok drugi

J = (0 → 0 → 0) → ((0 → 0) → 0) → 0 czyli do J = bool → ((0 → 0) → 0) → 0.

Teraz zredukujemy końcówkę((0 → 0) → 0) → 0 do typu word = (0 → 0) → (0 → 0) → 0 → 0.

(Potem zredukujemy J do typubool → word.)

(30)

Φ : [((0 → 0) → 0) → 0] → [(0 → 0) → (0 → 0) → 0 → 0]

Φ = λZ λf^0→0g^0→0x⁰. Z (λh^0→0. f (h(g (hx ))))

Kombinatory typu [(0 → 0) → 0] → 0 są takie: M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. . . . ϕ(λy_k. y_j))). Term M jest zdeterminowany przez liczby k i j.

Przykład: M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. ϕ(λy₃. ϕ(λy₄. y₂)))). WtedyΦ(M) = λfgx . f⁴(g (f²(x ))).

Opuszczamy szczegóły.

(31)

Φ : [((0 → 0) → 0) → 0] → [(0 → 0) → (0 → 0) → 0 → 0]

Kombinatory typu [(0 → 0) → 0] → 0 są takie:

M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. . . . ϕ(λy_k. y_j))).

Term M jest zdeterminowany przez liczbyk i j.

Przykład: M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. ϕ(λy₃. ϕ(λy₄. y₂)))). WtedyΦ(M) = λfgx . f⁴(g (f²(x ))).

(32)

Φ : [((0 → 0) → 0) → 0] → [(0 → 0) → (0 → 0) → 0 → 0]

Przykład: M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. ϕ(λy₃. ϕ(λy₄. y₂)))).

WtedyΦ(M) = λfgx . f⁴(g (f²(x ))). Opuszczamy szczegóły.

(33)

Φ : [((0 → 0) → 0) → 0] → [(0 → 0) → (0 → 0) → 0 → 0]

Przykład: M = λϕ^(0→0)→0. ϕ(λy₁. ϕ(λy₂. ϕ(λy₃. ϕ(λy₄. y₂)))).

WtedyΦ(M) = λfgx . f⁴(g (f²(x ))).

(34)

Krok drugi

Φ = λZ λf^0→0g^0→0x⁰. Z (λh^0→0. f (h(g (hx )))) M = λϕ^(0→0)→0. ϕ(λy1. ϕ(λy2. ϕ(λy3. ϕ(λy4. y2)))).

WtedyΦ(M) = λfgx . ϕ(λy₁. ϕ(λy₂. ϕ(λy₃. ϕ(λy₄. y₂)))), gdzie ϕ = λh^0→0. f (h(g (hx ))).

ϕ(λy₄. y₂) f ((λy4. y₂)(. . . )) → f (y₂); ϕ(λy3. fy2) f ((λy³. fy2)(. . . )) → f²(y2);

ϕ(λy₂. f²(y₂)) f ((λy2. f²(y₂))(g ((λy₂. f²(y₂))(x ))))

f³(g (f²(x )); ϕ(λy1. f³(g (f²(x ))) f ((λy¹. f³(g (f²(x )))(. . . )))

f⁴(g (f²(x ))). opuszczone

(35)

Krok drugi

ϕ(λy₄. y₂) f ((λy4. y₂)(. . . )) → f (y₂);

ϕ(λy3. fy2) f ((λy³. fy2)(. . . )) → f²(y2);

(36)

Krok drugi

ϕ(λy₄. y₂) f ((λy4. y₂)(. . . )) → f (y₂);

ϕ(λy3. fy2) f ((λy³. fy2)(. . . )) → f²(y2);

(37)

Krok drugi

ϕ(λy₄. y₂) f ((λy4. y₂)(. . . )) → f (y₂);

ϕ(λy3. fy2) f ((λy³. fy2)(. . . )) → f²(y2);

f³(g (f²(x ));

ϕ(λy1. f³(g (f²(x ))) f ((λy¹. f³(g (f²(x )))(. . . )))

(38)

Krok drugi

ϕ(λy₄. y₂) f ((λy4. y₂)(. . . )) → f (y₂);

ϕ(λy3. fy2) f ((λy³. fy2)(. . . )) → f²(y2);

f³(g (f²(x ));

ϕ(λy1. f³(g (f²(x ))) f ((λy¹. f³(g (f²(x )))(. . . )))

(39)

Krok trzeci

MamyJ = bool → J2 → 0, gdzie:

bool = 0 → 0 → 0 J₂ = (0 → 0) → 0.

W kroku drugim zredukowaliśmy typJ₂ → 0 do typu word = (0 → 0) → (0 → 0) → 0 → 0

używając Φ = λZ^J²^→0λf^0→0g^0→0x⁰. Z (λh^0→0f (h(g (hx )))) Teraz redukujemybool → J2 → 0dobool → wordużywając Ψ = λZ^bool→J²^→0λt^boolλf^0→0g^0→0x⁰. Zt(λh^0→0f (h(g (hx )))) czyliΨ = λZ^bool→J²^→0λt^bool. Φ(Zt).

(40)

Krok czwarty: redukcja bool → word do tree.

Typbool → word, czyli:

(0 → 0 → 0) → (0 → 0) → (0 → 0) → 0 → 0 odpowiada algebrze termów nad sygnaturą

t : 0 → 0 → 0, f , g : 0 → 0, c : 0.

Trzeba je zakodować jako zwykłe drzewa nad sygnaturą t : 0 → 0 → 0, c : 0.

Można to zrobić używając np.Θ : (bool → word) → tree:

Θ = λZ λt^0→0→0c⁰. Zt(λx tcx )(λx txc)(tcc)

(41)

Typy proste: semantyka

(42)

Semantics for finite types

Assumptions:

I Orthodox Church style;

I Only one atomic type0;

I Extensional equality =_βη.

(43)

Standard model M(A)

I Basic domainD0 = A;

I Function domains: Dσ→τ = Dσ → Dτ;

I Obvious semantics:

I [[x ]]v = v (x );

I [[MN]]_v = [[M]]_v([[N]]_v);

I [[λx^τ. M]]_v = λλd ∈D_τ. [[M]]_{v [x 7→d ]}.

(44)

Completeness

Theorem (Harvey Friedman):

Terms are βη-equal iff they are equal in M(N).

Proof:

Define partial surjections ϕ_σ : D_σ −◦ T^σ/₌_βη by induction: Forσ = 0 take ϕ0 : N → T⁰/=_βη to be any (total) surjection. (Terms of base type are represented by their numbers.) For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

ϕ_σ(ab) =_βη ϕ_{τ →σ}(a)ϕ_τ(b).

(45)

Completeness

Theorem (Harvey Friedman):

Proof:

Define partial surjectionsϕ_σ : D_σ −◦ T^σ/₌_βη by induction:

Forσ = 0 take ϕ0 : N → T⁰/=_βη to be any (total) surjection. (Terms of base type are represented by their numbers.) For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

(46)

Completeness

Theorem (Harvey Friedman):

Proof:

Forσ = 0 take ϕ0 : N → T⁰/=_βη to be any (total) surjection.

(Terms of base type are represented by their numbers.)

For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

(47)

Completeness

Theorem (Harvey Friedman):

Proof:

Forσ = 0 take ϕ0 : N → T⁰/=_βη to be any (total) surjection.

(Terms of base type are represented by their numbers.) For function types, we represent (the behaviour of) lambda-terms using integer functions, so that:

(48)

Completeness proof

Givenϕ_σ : D_σ −◦ T^σ/₌_βη and ϕ_τ : D_τ −◦ T^τ/₌_βη,

we say that a function f : D_τ → D_σ represents a term M^{τ →σ} when (informally) the following diagram commutes:

Dτ f //

ϕτ

Dσ ϕσ

T_τ/₌_βη

λλt. Mt

//T_σ/₌_βη

(49)

Completeness proof

I ϕ0 : N → T⁰/=_βη is any (total) surjection.

I ϕ_{τ →σ}(f ) = [M]₌_βη when f represents M. Abbreviation: Ifd ∈ D_σ, writed forϕ_σ(d ).

Main property:

If f and e are defined thenf (e) is defined and f e =_βη f (e)

(50)

Completeness proof

Lemma:

Takev so that v (x ) = x, for all x. Then M =_βη [[M]]_v, all M.

Main Proof:

LetM(N) |= M = N. Then [[M]]_v = [[N]]_v, for all v, in particular for v as above. Therefore

M =_βη [[M]]_v =_βη [[N]]_v =_βη N.

(51)

Completeness proof

Lemma:

Takev so that v (x ) = x, for all x. Then M =_βη [[M]]_v, all M.

Main Proof:

LetM(N) |= M = N. Then [[M]]_v = [[N]]_v, for all v, in particular for v as above. Therefore

M =_βη [[M]]_v =_βη [[N]]_v =_βη N.

(52)

Finite completeness

Łatwa obserwacja:

For every M and N there is k such that:

M =_βη N iff M(k) |= M = N.

Corollary:

Terms are βη-equal iff they are equal in all finite models.

(Konwencja: k = {0, 1, . . . , k − 1})

(53)

Finite completeness

Łatwa obserwacja:

For every M and N there is k such that:

Corollary:

(Konwencja: k = {0, 1, . . . , k − 1})

(54)

Finite completeness

Theorem (R. Statman):

For every M there is k such that, for all N: M =_βη N iff M(k) |= M = N.

Corollary:

(Konwencja: k = {0, 1, . . . , k − 1})

(55)

Finite completeness

Theorem (R. Statman):

For every M there is k such that, for all N: M =_βη N iff M(k) |= M = N.

Corollary:

(Konwencja: k = {0, 1, . . . , k − 1})

(56)

Finite completeness proof

It suffices to prove that

for every closed M : treethere is k such that, for all N : tree:

Indeed, for closedM : τ, consider Φ(M),

where Φis a reduction of τ to tree.

For non-closed terms, consider appropriate lambda-closures.

(57)

Finite completeness for tree

Letp(m)(n) = 2^m(2n + 1). Then p ∈ D_0→0→0 in M(N). Observe that p(m)(n) > m, n, for all m, n.

Term zamknięty typutree, to w istocie drzewo.

Wartość[[M]](p)(0) można uważać za numer tego drzewa. Ćwiczenie: Jaka liczba jest numerem drzewa

λpx . px (p(pxx )x )?

(58)

Finite completeness for tree

Wartość[[M]](p)(0) można uważać za numer tego drzewa. Ćwiczenie: Jaka liczba jest numerem drzewa

λpx . px (p(pxx )x )?

(59)

Finite completeness for tree

Wartość[[M]](p)(0) można uważać za numer tego drzewa.

Ćwiczenie: Jaka liczba jest numerem drzewa λpx . px (p(pxx )x )?

(60)

ForM : tree, define k = 2 + [[M]](p)(0), i.e. 2 + numer (M).

Letp⁰ : k → k → k be p „truncated” to values less than k. Thenp⁰ ∈ D0→0→0 in M(k).

SupposeM(k) |= M = N. Then in the model M(k):

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at mostk − 2. (Otherwise the rhs equalsk − 1.)

Therefore[[M]](p)(0) = [[N]](p)(0) holds also inM(N). It follows that M =_βη N.

(61)

Letp⁰ : k → k → k be p „truncated” to values less than k.

Thenp⁰ ∈ D0→0→0 in M(k).

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at mostk − 2. (Otherwise the rhs equalsk − 1.)

(62)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*)

But all numbers needed to verify (*) are at mostk − 2. (Otherwise the rhs equalsk − 1.)

(63)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at mostk − 2.

(Otherwise the rhs equalsk − 1.)

(64)

k − 2 = [[M]](p⁰)(0) = [[N]](p⁰)(0) (*) But all numbers needed to verify (*) are at mostk − 2.

(Otherwise the rhs equalsk − 1.)

Therefore[[M]](p)(0) = [[N]](p)(0) holds also inM(N). It follows that M = N.

(65)

Equality is not definable in simple types

There is noE : ωτ → ωσ → ωρ, such that for all p, q ∈ N: E p^ω^τq^ω^σ =_βη 0^ω^ρ iff p = q.

Proof:

By Statman’s thm., take k such that for all N : ω_ρ: M(k) |= 0^ω^ρ = N iff 0^ω^ρ =_βη N.

There arep 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k): [[E p^ω^τq^ω^σ]] = [[E ]][[p^ω^τ]][[q^ω^σ]] = [[E ]][[q^ω^τ]][[q^ω^σ]] =

[[E q^ω^τq^ω^σ]] = [[0^ω^ρ]] ThusM(k) |= E p^ω^τq^ω^σ = 0^ω^ρ, whence p = q.

(66)

Equality is not definable in simple types

Proof:

There arep 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k): [[E p^ω^τq^ω^σ]] = [[E ]][[p^ω^τ]][[q^ω^σ]] = [[E ]][[q^ω^τ]][[q^ω^σ]] =

(67)

Equality is not definable in simple types

Proof:

There arep 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k).

So inM(k): [[E p^ω^τq^ω^σ]] = [[E ]][[p^ω^τ]][[q^ω^σ]] = [[E ]][[q^ω^τ]][[q^ω^σ]] =

(68)

Equality is not definable in simple types

Proof:

There arep 6= q with [[p^ω^τ]] = [[q^ω^τ]] in M(k). So in M(k):

[[E p^ω^τq^ω^σ]] = [[E ]][[p^ω^τ]][[q^ω^σ]] = [[E ]][[q^ω^τ]][[q^ω^σ]] =

[[E q^ω^τq^ω^σ]] = [[0^ω^ρ]]

(69)

Plotkin’s problem

Givend ∈ D_τ in a finite model M(X ).

Is there a closed term M : τ with [[M]] = d?

More generally:

Let v (x₁) = e₁ ∈ D_σ₁, . . . , v (x_n) = e_n ∈ D_σ_n. Is there M such that [[M]]_v = d? (Is d definable from e₁, . . . , e_n?)

Fact: These decision problems are reducible to each other.

(70)

Plotkin’s problem

Givend ∈ D_τ in a finite model M(X ).

Is there a closed term M : τ with [[M]] = d?

More generally:

Let v (x₁) = e₁ ∈ D_σ₁, . . . , v (x_n) = e_n ∈ D_σ_n. Is there M such that [[M]]_v = d?

(Is d definable from e₁, . . . , e_n?)

(71)

Undecidablility of lambda-definability

Theorem (Ralph Loader, 1993):

Plotkin’s problem is undecidable.

Proof:

Reduction from the undecidable word problem for Semi-Thue systems.

Semi-Thue system: a finite set of rules C ⇒ D, where C , D ⊆ {a, b}^∗. Induces rewritingxCy → xDy, for any x, y. Word problem: Can a word w be rewritten to v in a finite number of steps?

(72)

Undecidablility of lambda-definability

Theorem (Ralph Loader, 1993):

Proof:

(73)

Undecidablility of lambda-definability

Theorem (Ralph Loader, 1993):

Proof:

(74)

Undecidablility of lambda-definability

Theorem (Ralph Loader, 1993):

Proof:

Kodujemy słowaw i v i reguły systemu jako elementy modelu.

Pytamy, czyv jest definiowalne z w i reguł.

(75)

Proof

TakeX = {a, b, L, R, ∗, 1, 0}. Encode any word w = o₁. . . o_n as a functionw : D₀ⁿ→ D₀, such that

I w (∗ · · · ∗ oi ∗ · · · ∗) = 1, if the i-th symbol in w is oi;

I w (∗ · · · ∗ LR ∗ · · · ∗) = 1;

I w (. . .) = 0, otherwise.

(76)

How does it work?

Forw = w1Cw2 we have w = λλ~x λλ~y λλ~z. w (~x )(~y )(~z).

Fix~x , ~z and consider the function g = λλ~y . w (~x )(~y )(~z). It “accepts” the following strings (depending on~x , ~z):

~x ~y ~z

∗ · · · ∗ o_i ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ same as C ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗ o_i∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ L R ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ L R ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗ LR ∗ · · · ∗

(77)

How does it work?

Fix~x , ~z and consider the function g = λλ~y . w (~x )(~y )(~z).

It “accepts” the following strings (depending on~x , ~z):

~x ~y ~z

∗ · · · ∗ o_i ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ same as C ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗ o_i∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ L R ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ L R ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗ LR ∗ · · · ∗

(78)

How does it work?

It “accepts” the following strings (depending on~x , ~z):

~x ~y ~z

∗ · · · ∗ o_i ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ same as C ∗ · · · ∗

∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗ o_i∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ ∗ · · · ∗ ∗ · · · ∗

∗ · · · ∗ L R ∗ · · · ∗ ∗ · · · ∗

(79)

How does it work?

Depending on~x , ~z, the function g is as follows:

~x g ~z

∗ · · · ∗ oi ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ{∗···∗} ∗ · · · ∗ oi ∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗

∗ · · · ∗ L χ_{{R∗···∗}} ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗L}} R ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗ LR ∗ · · · ∗

(80)

How to encode a rule F = (C ⇒ D)?

What will change in this table if we replacew₁Cw₂ by w₁Dw₂?

~

x g ~z

∗ · · · ∗ o_i ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ{∗···∗} ∗ · · · ∗ oi ∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ L χ_{{R∗···∗}} ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗L}} R ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗ LR ∗ · · · ∗

other χ_∅ other

(81)

How to encode a rule F = (C ⇒ D)?

What will change in this table if we replacew₁Cw₂ by w₁Dw₂?

~

x g ~z

∗ · · · ∗ o_i ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ C ∗ · · · ∗

∗ · · · ∗ χ{∗···∗} ∗ · · · ∗ oi ∗ · · · ∗

∗ · · · ∗ LR ∗ · · · ∗ χ{∗···∗} ∗ · · · ∗

∗ · · · ∗ L χ{R∗···∗} ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗L}} R ∗ · · · ∗

∗ · · · ∗ χ_{{∗···∗}} ∗ · · · ∗ LR ∗ · · · ∗

(82)

How to encode a rule F = (C ⇒ D)

Every ruleF = (C ⇒ D) is encoded as a function F : (D₀^m → D0) → (D₀ⁿ → D0),

wherem = |C | and n = |D|. We take:

I F (χ{∗···∗}) = χ{∗···∗};

I F (χ{R∗···∗}) = χ{R∗···∗};

I F (χ_{{∗···∗L}}) = χ_{{∗···∗L}};

I F (C ) = D;

(83)

Claim

A word w can be rewritten to v iff the element v of M(X ) is definable fromw and the functions F encoding the rules.

The easy part: Letw = w1Cw2 rewrite to v = w1Dw2

usingF = (C ⇒ D). Assume that term W defines w. Thenv is definable by

V = λ~x ~u~z. F (λ~y . W ~x~y ~z)~u, (*) It follows that codes of reachable words are definable.

The hard part: And conversely.

(84)

Claim

(85)

Claim

(86)

Inhabitation for intersection types

Theorem

The inhabitation problem for intersection types is undecidable.

Proof: Reduction from definability.

Encode elementsd of M(X )as intersection typesτ_d:

I If d ∈ D₀ then τ_d = d.

I If d ∈ Dα→β then τd =T

e∈Dα(τe → τde). For a valuationv in M(X ), take Γ_v(x ) = τ_{v (x )}. Main Lemma: [[M]]_v = d iff Γ_v ` M : τ_d.

(87)

Inhabitation for intersection types

Theorem

Encode elementsd of M(X )as intersection typesτ_d:

I If d ∈ D₀ then τ_d = d.

I If d ∈ Dα→β then τd =T

e∈Dα(τe → τde). For a valuationv in M(X ), take Γ_v(x ) = τ_{v (x )}. Main Lemma: [[M]]_v = d iff Γ_v ` M : τ_d.

(88)

Inhabitation for intersection types

Theorem

Encode elementsd of M(X ) as intersection typesτ_d:

I If d ∈ D0 then τd = d.

I If d ∈ D_α→β then τ_d =T

e∈Dα(τ_e → τ_de).

For a valuationv in M(X ), take Γ_v(x ) = τ_{v (x )}. Main Lemma: [[M]]_v = d iff Γ_v ` M : τ_d.

(89)

Inhabitation for intersection types

Theorem

Encode elementsd of M(X ) as intersection typesτ_d:

I If d ∈ D0 then τd = d.

I If d ∈ D_α→β then τ_d =T

e∈Dα(τ_e → τ_de).

For a valuationv in M(X ), take Γ_v(x ) = τ_{v (x )}. Main Lemma: [[M]]_v = d iff Γ_v ` M : τ_d.

(90)

Higher-order unification

Problem:

Given Church-style (normal) terms M,N of the same type with some variables x₁^σ¹, . . . , x_n^σⁿ called unknowns. (There may be other variables called constants or parameters.) Are there termsP₁^σ¹, . . . , P_n^σⁿ such that

M[x1 := P1, . . . x_n:= P_n] =_βη N[x1 := P1, . . . x_n := P_n]? Non-essential generalization to finite systems of equations.

Examples

(constantsa, b : p, f : p → p → p,

unknowns F : p → p,G : p → p → p)

I fa(Fa) = F (faa)has solutions λx .fa(fa(fa(· · · (fax ) · · · ))).

I Gab = fa(Gab)has no solution.

(91)

Higher-order unification

Problem:

Given Church-style (normal) terms M,N of the same type with some variablesx₁^σ¹, . . . , x_n^σⁿ called unknowns.

(There may be other variables called constants or parameters.) Are there termsP₁^σ¹, . . . , P_n^σⁿ such that

M[x1 := P1, . . . x_n := P_n] =_βη N[x1 := P1, . . . x_n := P_n]?

Non-essential generalization to finite systems of equations.

Examples

(92)

Higher-order unification

Problem:

Examples

(93)

Higher-order unification

Problem:

Examples

(94)

Higher-order unification

Problem:

Examples

(95)

Example 1

The equationfa(Fa) = F (faa) has solutions λx .fa(fa(fa(· · · (fax ) · · · ))).

f = F F (x ) := f

a F f a f

a a a a x

(96)

Example 2

The equationGab = fa(Gab) has no solution.

G = f

a b a G

a b

(97)

Rząd (order)

Rząd typu:

I order (p) = 0;

I order (σ → τ ) = max{order (σ) + 1, order (τ )}.

Uwaga:

order (σ1→ · · · →σ_n→p) = 1 + max{order (σ_n) | n = 1, . . . , n}

Unificationof order n has unknowns of order n − 1.

(98)

Rząd (order)

Rząd typu:

I order (p) = 0;

Uwaga:

order (σ₁→ · · · →σ_n→p) = 1 + max{order (σ_n) | n = 1, . . . , n}

(99)

Rząd (order)

Rząd typu:

I order (p) = 0;

Uwaga:

order (σ₁→ · · · →σ_n→p) = 1 + max{order (σ_n) | n = 1, . . . , n}

(100)

Undecidability

Theorem 1 (C.L. Lucchesi’72, G. Huet’73):

The third-order unification is undecidable.

Theorem 2 (W. Goldfarb’81):

The second-order unification is undecidable.

Theorem 3 (A. Schubert’97):

Nierozstrzygalność drugiego rzędu nawet wtedy, gdy niewiadome nie są zagnieżdżone.

(101)

Undecidability

(102)

Undecidability

(103)

X problem Hilberta

Twierdzenie (Matjasiewicz)

Następujący problem jest nierozstrzygalny:

Dany wielomianw (~x ) o współczynnikach całkowitych. Czy równaniew (~x ) = 0ma rozwiązanie w liczbach całkowitych?