Claude Kirchner

Florent Kirchner

Helene Kirchner

Strategic Computation and Deduction

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

✶✳ ❆ ✜rst st❛♥❞❛r❞ ❡①❛♠♣•❡✿

A lc = a φ1 ' ' φ2 b φ3 h h φ4 c d ✷✳ ❚❤❡ ✐♥t❡r❡st ♦❢ ✉s✐♥❣ ❣r❛♣❤ ✐♥st❡❛❞ ♦❢ ❜✐♥❛r② r❡•❛t✐♦♥s ✐s ❡①❡♠♣•✐✜❡❞ ❜② A c = a φ1 Q Q φ2 ❚❤❡ ♥❡①t ❞❡✜♥✐t✐♦♥s ❝❛♥ ❜❡ s❡❡♥ ❛s ❛ r❡♥❛♠✐♥❣ ♦❢ ✉s✉❛• ♦♥❡s ✐♥ ❣r❛♣❤ t❤❡♦r②✳ ❚❤❡✐r ✐♥t❡r❡st ✐s t♦ ❛••♦✇ ✉s t♦ ❞❡✜♥❡ ✉♥✐❢♦r♠•② t❡r♠ r❡✇r✐t✐♥❣ ❞❡r✐✈❛t✐♦♥s ❛♥❞ str❛t❡❣✐❡s✳ ■❢ t❤❡ ❝♦♥❝❡♣ts ❛r❡ ♥♦t ♦r✐❣✐♥❛•✱ t❤❡✐r ♣r❡s❡♥t❛✲ t✐♦♥ ✐s✳ ❉❊❋■◆■❚■❖◆ ✸ ✭❉❡r✐✈❛t✐♦♥✮✳ ❋♦r ❛ ❣✐✈❡♥ ❆|❙ A✿
✶✳ ❆ r❡❞✉❝t✐♦♥ st❡♣ ✐s ❛ •❛❜❡••❡❞ ❡❞❣❡ φ t♦❣❡t❤❡r ✇✐t❤ ✐ts s♦✉r❝❡ a ❛♥❞ t❛r❣❡t b✳ ❚❤✐s ✐s ✇r✐tt❡♥ a φ A b✱ ♦r s✐♠♣•② a φ b ✇❤❡♥ ✉♥❛♠❜✐❣✉♦✉s✳ ✷✳ ❆♥ A✲❞❡r✐✈❛t✐♦♥ ♦r A✲r❡❞✉❝t✐♦♥ s❡q✉❡♥❝❡ ✐s ❛ ♣❛t❤ π ✐♥ t❤❡ ❣r❛♣❤ A✳ ✸✳ ❲❤❡♥ ✐t ✐s ✜♥✐t❡✱ ❛♥ A✲❞❡r✐✈❛t✐♦♥ π ❝❛♥ ❜❡ ✇r✐tt❡♥ a 0 φ0 a 1 φ1 a 2 . . . φn-1 a n ❛♥❞ ✇❡ s❛② t❤❛t a 0 r❡❞✉❝❡s t♦ a n ❜② t❤❡ ❞❡r✐✈❛t✐♦♥ π = φ 0 φ 1 . . . φ n-1 ❀ t❤✐s ✐s ❛•s♦ ❞❡♥♦t❡❞ a 0 φ0φ1...φn-1 a n ♦r s✐♠♣•②

a 0 π a n ✳ ❲❡ ❝❛•• n t❤❡ •❡♥❣t❤ ♦❢ π✳ ✭❛✮ ❚❤❡ s♦✉r❝❡ ♦❢ π ✐s t❤❡ ♦❜•❡❝t a 0 ❛♥❞ ✐ts ❞♦♠❛✐♥ ✐s ❞❡✜♥❡❞ ❛s t❤❡ s✐♥❣•❡t♦♥ ❞♦♠(π) = {a 0 }✳ ✭❜✮ ❚❤❡ t❛r❣❡t ♦❢ π ✐s t❤❡ ♦❜•❡❝t a n ❛♥❞ t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦❢ t❤❡ ❞❡r✐✈❛✲ t✐♦♥ π t♦ a 0 ✐s t❤❡ s✐♥❣•❡t♦♥ ❞❡♥♦t❡❞ (π a 0 ) = {a n }✳ ❚❤✐s ✐s ❛•s♦ ❞❡♥♦t❡❞ s✐♠♣•② πa 0 ✇❤❡♥ t❤❡r❡ ✐s ♥♦ s②♥t❛❝t✐❝ ❛♠❜✐❣✉✐t②✳ ✹✳ ❚❤❡ s❡t ♦❢ ❛•• ❞❡r✐✈❛t✐♦♥s ✐s ❞❡♥♦t❡❞ D(A)✳
✺✳ ❆ ❞❡r✐✈❛t✐♦♥ ✐s ❡♠♣t② ✇❤❡♥ ✐ts •❡♥❣t❤ ✐s ③❡r♦✱ ✐♥ ✇❤✐❝❤ ❝❛s❡ ✐ts s♦✉r❝❡ ❛♥❞ t❛r❣❡t ❛r❡ t❤❡ s❛♠❡✳ ❚❤❡ ❡♠♣t② ❞❡r✐✈❛t✐♦♥ ✐ss✉❡❞ ❢r♦♠ a ✐s ❞❡✲ ♥♦t❡❞

id a ✳ ✻✳ ❚❤❡ ❝♦♥❝❛t❡♥❛t✐♦♥ ♦❢ t✇♦ ❞❡r✐✈❛t✐♦♥s π 1 ❛♥❞ π 2 ✐s ❞❡✜♥❡❞ ✇❤❡♥ ❞♦♠(π 1 ) = {a} ❛♥❞ π 1 a = ❞♦♠(π 2 )✳ ❚❤❡♥ π 1 ; π 2 ❞❡♥♦t❡s t❤❡ ♥❡✇ A✲❞❡r✐✈❛t✐♦♥ a π1 A b π2 A c ❛♥❞ ((π 1 ; π 2 ) a) = (π 2 (π 1 a)) = {c}✳ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✺ ◆♦t❡ t❤❛t ❛♥ A✲❞❡r✐✈❛t✐♦♥ ✐s t❤❡ ❝♦♥❝❛t❡♥❛t✐♦♥ ♦❢ ✐ts r❡❞✉❝t✐♦♥ st❡♣s✳ ❊❳❆▼P▲❊ ✹✳ ❋♦••♦✇✐♥❣ t❤❡ ♣r❡✈✐♦✉s ❡①❛♠♣•❡s✱ ✇❡ ❤❛✈❡✿ ✶✳ D(A lc ) ⊃ {id a , φ 1 , φ 1 φ 3 , φ 1 φ 4 , φ 1 φ 3 φ 1 , (φ 1 φ 3 ) n , (φ 1 φ 3 ) ω , . . .}✱ ✇❤❡r❡ φ n ❞❡♥♦t❡s t❤❡ n✲st❡♣s ✐t❡r❛t✐♦♥ ♦❢ φ ❛♥❞ φ ω ❞❡♥♦t❡s t❤❡ ✐♥✜♥✐t❡ ✐t❡r✲ ❛t✐♦♥ ♦❢ φ❀ ✷✳ D(A c ) ⊃ {φ 1 , φ 2 , φ 1 φ 2 , . . . , (φ 1 ) ω , (φ 2 ) ω , . . .}✳ ❚❤❡ ❢♦••♦✇✐♥❣ ❞❡✜♥✐t✐♦♥s st❛t❡ ❣❡♥❡r❛• ♣r♦♣❡rt✐❡s ♦❢ ❛♥ ❆|❙✳ ❉❊❋■◆■❚■❖◆ ✺ ✭❚❡r♠✐♥❛t✐♦♥✮✳ ❋♦r ❛ ❣✐✈❡♥ ❆|❙ A = (O, S)✿ • A ✐s t❡r♠✐♥❛t✐♥❣ ✭♦r str♦♥❣•② ♥♦r♠❛•✐③✐♥❣✮ ✐❢ ❛•• ✐ts ❞❡r✐✈❛t✐♦♥s ❛r❡ ♦❢ ✜♥✐t❡ •❡♥❣t❤❀ • ❆♥ ♦❜•❡❝t a ✐♥ O ✐s ♥♦r♠❛•✐③❡❞ ✇❤❡♥ t❤❡ ❡♠♣t② ❞❡r✐✈❛t✐♦♥ ✐s t❤❡ ♦♥•② ♦♥❡ ✇✐t❤ s♦✉r❝❡ a ✭❡✳❣✳✱ a ✐s t❤❡ s♦✉r❝❡ ♦❢ ♥♦ ❡❞❣❡✮❀ • ❆ ❞❡r✐✈❛t✐♦♥ ✐s ♥♦r♠❛•✐③✐♥❣ ✇❤❡♥ ✐ts t❛r❣❡t ✐s ♥♦r♠❛•✐③❡❞❀ • ❆♥ ❆|❙ ✐s ✇❡❛❦•② t❡r♠✐♥❛t✐♥❣ ✐❢ ❡✈❡r② ♦❜•❡❝t a ✐s t❤❡ s♦✉r❝❡ ♦❢ ❛ ♥♦r♠❛•✐③✐♥❣ ❞❡r✐✈❛t✐♦♥✳ ❉❊❋■◆■❚■❖◆ ✻ ✭❈♦♥✢✉❡♥❝❡✮✳ ❆♥ ❆|❙ A = (O, S) ✐s ❝♦♥✢✉❡♥t ✐❢ ❢♦r ❛•• ♦❜•❡❝ts a✱ b✱ c ✐♥ O✱ ❛♥❞ ❛•• A✲❞❡r✐✈❛t✐♦♥s π 1 ❛♥❞ π 2 ✱ ✇❤❡♥ a π1 b ❛♥❞ a π2 c✱ t❤❡r❡ ❡①✐st d ✐♥ O ❛♥❞ t✇♦ A✲❞❡r✐✈❛t✐♦♥s π 3 , π 4 s✉❝❤ t❤❛t c π3 d ❛♥❞ b π4 d✳ ✸ ❆❜str❛❝t str❛t❡❣✐❡s ❲❡ ✉s❡ ❛ ❣❡♥❡r❛• ❞❡✜♥✐t✐♦♥✱ ❝♦♠♣•✐❛♥t ✇✐t❤ ❬✸✹( ❛♥❞ s•✐❣❤t•② ❞✐✛❡r❡♥t ❢r♦♠ t❤❡ ♦♥❡ ✉s❡❞ ✐♥✱ ❡✳❣✳✱ ❬✺✹(✳ ❉❊❋■◆■❚■❖◆ ✼ ✭❆❜str❛❝t ❙tr❛t❡❣②✮✳ ❋♦r ❛ ❣✐✈❡♥ ❆|❙ A✿ ✶✳ ❆♥ ❛❜str❛❝t str❛t❡❣② ζ ✐s ❛ s✉❜s❡t ♦❢ t❤❡ s❡t ♦❢ ❛•• ❞❡r✐✈❛t✐♦♥s ✭✜♥✐t❡ ♦r ♥♦t✮ ♦❢ A✳ ✷✳ ❆♣♣•②✐♥❣ t❤❡ str❛t❡❣② ζ ♦♥ ❛♥ ♦❜•❡❝t a ✐s ❞❡♥♦t❡❞ ζa✳ ■t ❞❡♥♦t❡s t❤❡ s❡t ♦❢ ❛•• ♦❜•❡❝ts t❤❛t ❝❛♥ ❜❡ r❡❛❝❤❡❞ ❢r♦♠ a ✉s✐♥❣ ❛ ❞❡r✐✈❛t✐♦♥ ✐♥ ζ✿ ζa = {b | ∃π ∈ ζ s✉❝❤ t❤❛t a π b} = {πa | π ∈ ζ} ❲❤❡♥ ♥♦ ❞❡r✐✈❛t✐♦♥ ✐♥ ζ ❤❛s s♦✉r❝❡ a✱ ✇❡ s❛② t❤❛t t❤❡ str❛t❡❣② ❛♣♣•✐✲ ❝❛t✐♦♥ ♦♥ a ❢❛✐•s✳ ✸✳ ❆♣♣•②✐♥❣ t❤❡ str❛t❡❣② ζ ♦♥ ❛ s❡t ♦❢ ♦❜•❡❝ts ❝♦♥s✐sts ✐♥ ❛♣♣•②✐♥❣ ζ t♦ ❡❛❝❤ ❡•❡♠❡♥t a ♦❢ t❤❡ s❡t✳ ❚❤❡ r❡s✉•t ✐s t❤❡ ✉♥✐♦♥ ♦❢ ζa ❢♦r ❛•• a ✐♥ t❤❡ s❡t ♦❢ ♦❜•❡❝ts✳ ✹✳ ❚❤❡ ❞♦♠❛✐♥ ♦❢ ❛ str❛t❡❣② ✐s t❤❡ s❡t ♦❢ ♦❜•❡❝ts t❤❛t ❛r❡ s♦✉r❝❡ ♦❢ ❛ ❞❡r✐✈❛t✐♦♥ ✐♥ ζ✿ ❞♦♠(ζ ) = δ∈ζ ❞♦♠(δ) ✺✳ ❚❤❡ str❛t❡❣② t❤❛t ❝♦♥t❛✐♥s ❛•• t❤❡ ❡♠♣t② ❞❡r✐✈❛t✐♦♥s ✐s ❞❡♥♦t❡❞ Id✿ Id = {id a | a ∈ O} ❲✐t❤ t❤✐s ❞❡✜♥✐t✐♦♥✱ ❛ str❛t❡❣② t❤❛t ❝♦♥t❛✐♥s ♦♥•② ✐♥✜♥✐t❡ ❞❡r✐✈❛t✐♦♥s ❢r♦♠ s♦✉r❝❡ a ✐s ♥♦t ❞❡✜♥❡❞ ♦♥ a✳ ❚❤✐s ❤❛s t♦ ❜❡ ❞✐st✐♥❣✉✐s❤❡❞ ❢r♦♠ t❤❡ ❝❛s❡ ✇❤❡r❡ ❛ str❛t❡❣② ❝♦♥t❛✐♥s ♥♦ ❞❡r✐✈❛t✐♦♥s ❢r♦♠ s♦✉r❝❡ a ❛♥❞ r❡t✉r♥s t❤❡ ❡♠♣t② s❡t ∅✱ ✐✳❡✳✱ t❤❡ str❛t❡❣② ❛♣♣•✐❝❛t✐♦♥ ❢❛✐•s✳ ❚❤❡ ❡♠♣t② s❡t ♦❢ ❞❡r✐✈❛t✐♦♥s ✐s ❛ str❛t❡❣② ❝❛••❡❞ Fail ❀ ✐ts ❛♣♣•✐❝❛t✐♦♥ ❛•✇❛②s ❢❛✐•s✳ ◆♦t✐❝❡ ✜♥❛••② t❤❛t ✐♥st❡❛❞ ♦❢ r❡t✉r♥✐♥❣ s❡ts ♦❢ r❡s✉•ts✱ ✇❡ ♠✐❣❤t ❞❡✜♥❡ str❛t❡❣✐❡s t♦ r❡t✉r♥ ♠✉•t✐s❡ts ♦r ❡✈❡♥ •✐st ♦r ❛♥② ❛♣♣r♦♣r✐❛t❡ ❞❛t❛ str✉❝t✉r❡✳ ❊❳❆▼P▲❊ ✽ ✭❊①❛♠♣•❡ ✷ ❝♦♥t✐♥✉❡❞✮✳ ❋♦r A lc ✱ •❡t ✉s ❞❡✜♥❡ ❛♥❞ ❡①❛♠✐♥❡ ❛ ❢❡✇ str❛t❡❣✐❡s✿ ✶✳ ζ 1 = D(A lc )✱ ✐✳❡✳✱ ❛•• t❤❡ ❞❡r✐✈❛t✐♦♥s✳ ❙♦ ✇❡ ❤❛✈❡ ❢♦r ❡①❛♠♣•❡✿ ζ 1 a = {a, b, c, d}✳ ■❢ ♠✉•t✐s❡ts ♦❢ r❡s✉•ts ❛r❡ ❝♦♥s✐❞❡r❡❞✱ ζ 1 a = {a, a, ..., b, c, d} ✐♥ ✇❤✐❝❤ a ♦❝❝✉rs ❢♦r ❡❛❝❤ ✜♥✐t❡ ❞❡r✐✈❛t✐♦♥ ✇❤✐❝❤ ❛♣♣r♦①✐♠❛t❡s (φ 1 φ 3 ) ω ✳ ✷✳ ζ 2 = ∅(= Fail )✿ ❢❛✐•✉r❡✱ ♥♦ ❛♣♣•✐❝❛❜•❡ ❞❡r✐✈❛t✐♦♥✱ ✐✳❡✳✱ ❢♦r ❛•• x ✐♥ O lc ✱ ζ 2 x = ∅✳ ✸✳ ζ 3 = {(φ 1 φ 3 ) * φ 4 }✱ a ❛•✇❛②s ❝♦♥✈❡r❣❡s t♦ d✿ ζ 3 a = {d}❀ b ✐s ♥♦t tr❛♥s❢♦r♠❡❞ ✭❛s ✇❡•• ❛s c ❛♥❞ d✮✿ ζ 3 b = ∅✳ ✹✳ ❚❤❡ r❡s✉•t ♦❢ ((φ 1 φ 3 ) ω a) ✐s t❤❡ ❡♠♣t② s❡t✳ ❚❤❡ st❛♥❞❛r❞ ♥♦t✐♦♥s ♦❢ ❆|❙ t❡r♠✐♥❛t✐♦♥ ❛♥❞ ❝♦♥✢✉❡♥❝❡ ♠✉st ❜❡ ❝❛r❡✲ ❢✉••② ❡①t❡♥❞❡❞ t♦ ❛❜str❛❝t str❛t❡❣✐❡s✳ ❉❊❋■◆■❚■❖◆ ✾ ✭❚❡r♠✐♥❛t✐♦♥ ✉♥❞❡r str❛t❡❣②✮✳ ❋♦r ❛ ❣✐✈❡♥ ❆|❙ A = (O, S) ❛♥❞ str❛t❡❣② ζ✿ • A ✐s ζ✲t❡r♠✐♥❛t✐♥❣ ✐❢ ❛•• ❞❡r✐✈❛t✐♦♥s ✐♥ ζ ❛r❡ ♦❢ ✜♥✐t❡ •❡♥❣t❤❀ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✼ • ❆♥ ♦❜•❡❝t a ✐♥ O ✐s ζ✲♥♦r♠❛•✐③❡❞ ✇❤❡♥ t❤❡ ❡♠♣t② ❞❡r✐✈❛t✐♦♥ ✐s t❤❡ ♦♥•② ♦♥❡ ✐♥ ζ ✇✐t❤ s♦✉r❝❡ a❀ • ❆ ❞❡r✐✈❛t✐♦♥ ✐s ζ✲♥♦r♠❛•✐③✐♥❣ ✇❤❡♥ ✐ts t❛r❣❡t ✐s ζ✲♥♦r♠❛•✐③❡❞❀ • ❆♥ ❆|❙ ✐s ✇❡❛❦•② ζ✲t❡r♠✐♥❛t✐♥❣ ✐❢ ❡✈❡r② ♦❜•❡❝t a ✐s t❤❡ s♦✉r❝❡ ♦❢ ❛ ζ✲♥♦r♠❛•✐③✐♥❣ ❞❡r✐✈❛t✐♦♥✳ ❊❳❆▼P▲❊ ✶✵ ✭❊①❛♠♣•❡ ✷ ❝♦♥t✐♥✉❡❞✮✳ •✐✈❡♥ A lc ❛♥❞ t❤❡ str❛t❡❣② ζ ❞❡✜♥❡❞ ❛s a φ1 b φ4 d✱ b ✐s ζ✲♥♦r♠❛•✐③❡❞ s✐♥❝❡ t❤❡r❡ ✐s ♥♦ ❞❡r✐✈❛t✐♦♥ ✐♥ ζ ✇✐t❤ s♦✉r❝❡ b✳ ■t ❝♦✉•❞ ❜❡ t❡♠♣t✐♥❣ t♦ ❣❡♥❡r❛•✐③❡ ❉❡✜♥✐t✐♦♥ ✻ ❛s ❢♦••♦✇s✿ ❆♥ ❆|❙ A = (O, S) ✐s ❝♦♥✢✉❡♥t ✉♥❞❡r str❛t❡❣② ζ ✐❢ ❢♦r ❛•• ♦❜•❡❝ts a✱ b✱ c ✐♥ O✱ ❛♥❞ ❛•• A✲❞❡r✐✈❛t✐♦♥s π 1 ❛♥❞ π 2 ✐♥ ζ✱ ✇❤❡♥ a π1 b ❛♥❞ a π2 c t❤❡r❡ ❡①✐sts d ✐♥ O ❛♥❞ t✇♦ A✲❞❡r✐✈❛t✐♦♥s π 3 , π 4 ✐♥ ζ s✉❝❤ t❤❛t c π3 d ❛♥❞ b π4 d✳ ❍♦✇❡✈❡r t❤✐s ❣❡♥❡r❛•✐③❛t✐♦♥ ✐s ♥♦t ❝♦rr❡❝t s✐♥❝❡ ♥♦t❤✐♥❣ ❡♥s✉r❡s t❤❛t t❤❡ ❞❡r✐✈❛t✐♦♥s c π3 d ❛♥❞ b π4 d ❜❡•♦♥❣ t♦ t❤❡ str❛t❡❣②✳ ❚❤✐s •❡❛❞s t♦ t✇♦ ♣♦ss✐❜•❡ ❞❡✜♥✐t✐♦♥s ♦❢ r❡s♣❡❝t✐✈❡•② ✇❡❛❦ ❛♥❞ str♦♥❣ ❝♦♥✢✉❡♥❝❡ ✉♥❞❡r str❛t❡❣②✳ ❉❊❋■◆■❚■❖◆ ✶✶ ✭❲❡❛❦ ❈♦♥✢✉❡♥❝❡ ✉♥❞❡r str❛t❡❣②✮✳ ❆♥ ❆|❙ A = (O, S) ✐s ✇❡❛❦•② ❝♦♥✢✉❡♥t ✉♥❞❡r str❛t❡❣② ζ ✐❢ ❢♦r ❛•• ♦❜•❡❝ts a✱ b✱ c ✐♥ O✱ ❛♥❞ ❛•• A✲❞❡r✐✈❛t✐♦♥s π 1 ❛♥❞ π 2 ✐♥ ζ✱ ✇❤❡♥ a π1 b ❛♥❞ a π2 c t❤❡r❡ ❡①✐sts d ✐♥ O ❛♥❞ t✇♦ A✲❞❡r✐✈❛t✐♦♥s π ′ 3 , π ′ 4 ✐♥ ζ s✉❝❤ t❤❛t π ′ 3 : a b d ❛♥❞ π ′ 4 : a c d✳ ❉❊❋■◆■❚■❖◆ ✶✷ ✭❙tr♦♥❣ ❈♦♥✢✉❡♥❝❡ ✉♥❞❡r str❛t❡❣②✮✳ ❆♥ ❆|❙ A = (O, S) ✐s str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r str❛t❡❣② ζ ✐❢ ❢♦r ❛•• ♦❜•❡❝ts a✱ b✱ c ✐♥ O✱ ❛♥❞ ❛•• A✲❞❡r✐✈❛t✐♦♥s π 1 ❛♥❞ π 2 ✐♥ ζ✱ ✇❤❡♥ a π1 b ❛♥❞ a π2 c t❤❡r❡ ❡①✐sts d ✐♥ O ❛♥❞ t✇♦ A✲❞❡r✐✈❛t✐♦♥s π 3 , π 4 ✐♥ ζ s✉❝❤ t❤❛t✿ ✶✳ b π3 d ❛♥❞ c π4 d❀ ✷✳ π 1 ; π 3 ❛♥❞ π 2 ; π 4 ❜❡•♦♥❣ t♦ ζ✳ ❊❳❆▼P▲❊ ✶✸ ✭❊①❛♠♣•❡ ✷ ❝♦♥t✐♥✉❡❞✮✳ ▲❡t ✉s ❛❣❛✐♥ ❝♦♥s✐❞❡r A lc ❛♥❞ t❤❡ ❢♦••♦✇✐♥❣ ✈❛r✐♦✉s str❛t❡❣✐❡s✿ ✶✳ ζ 1 = D(A lc )✱ ✐✳❡✳✱ ❛•• t❤❡ ❞❡r✐✈❛t✐♦♥s✳ A lc ✐s ♥❡✐t❤❡r ✇❡❛❦•② ♥♦r str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r ζ 1 ✿ •✉st ❝♦♥s✐❞❡r π 1 : a φ1 b φ4 d ❛♥❞ π 2 : a φ2 c✳ ✷✳ ζ 2 = ∅(= Fail )✿ A lc ✐s tr✐✈✐❛••② ❜♦t❤ ✇❡❛❦•② ❛♥❞ str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r ζ 2 ✳ ✸✳ ζ 3 = {(φ 1 φ 3 ) * φ 4 }✿ A lc ✐s ❛•s♦ ✇❡❛❦•② ❛♥❞ str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r ζ 3 ✳ ✹✳ ❋♦r ❛ ❞✐✛❡r❡♥t r❡❛s♦♥✱ t❤✐s ✐s ❛•s♦ t❤❡ ❝❛s❡ ❢♦r ζ 4 = (φ 1 φ 3 ) ω ✇❤♦s❡ r❡s✉•t ✐s t❤❡ ❡♠♣t② s❡t✳ ❚♦ ✉♥❞❡rst❛♥❞ t❤❡ ❞✐✛❡r❡♥❝❡ ❜❡t✇❡❡♥ ✇❡❛❦ ❛♥❞ str♦♥❣ ❝♦♥✢✉❡♥❝❡ •❡t ✉s ❝♦♥✲ s✐❞❡r O = {a, b, c, d} ❛♥❞ r❡❞✉❝t✐♦♥ st❡♣s φ 1 , φ 2 , φ 3 , φ 4 , φ ′ 1 , φ ′ 2 , φ ′ 3 , φ ′ 4 ✳ ❚❤✐s ❆|❙ A lc ✐s ✇❡❛❦•② ❛♥❞ str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r t❤❡ str❛t❡❣② ζ = {a φ1 b, a φ2 c, b φ3 d, c φ4 d, a φ1 b φ3 d, a φ2 c φ4 d}✱ ❜✉t ✐s ♥♦t ✉♥❞❡r ζ = {a φ1 b, a φ2 c, b φ3 d, c φ4 d}✳ A ✐s ✇❡❛❦•② ❜✉t ♥♦t str♦♥❣•② ❝♦♥✢✉❡♥t ✉♥❞❡r t❤❡ str❛t❡❣② ζ = {a φ1 b, a φ2 c, b φ3 d, c φ4 d, a φ ′ 1 b φ ′ 3 d, a φ ′ 2 c φ ′ 4 d}✳ ✹ ❚❤❡ r❡✇r✐t✐♥❣ ❝❛•❝✉•✉s ❚❤❡ r❡✇r✐t✐♥❣ ❝❛•❝✉•✉s ♦r ρ✲❝❛•❝✉•✉s ❣❡♥❡r❛•✐③❡s t❡r♠ r❡✇r✐t✐♥❣ ❛♥❞ •❛♠❜❞❛✲ ❝❛•❝✉•✉s✳ ■t ❤❛s ❜❡❡♥ ✐♥tr♦❞✉❝❡❞ ✐♥ ❬✶✹(✳ ❲❡ r❡❝❛•• ❤❡r❡ t❤❡ ♠❛✐♥ s②♥t❛❝t✐❝ ✐♥❣r❡❞✐❡♥ts ♥❡❝❡ss❛r② t♦ s❡t✲✉♣ t❤❡ ❢r❛♠❡✇♦r❦ ❞❡✈❡•♦♣❡❞ ✐♥ t❤✐s ♣❛♣❡r✱ ✉s✐♥❣ ❛ s②♥t❛① t❤❛t r❡str✐❝ts ♣❛tt❡r♥s t♦ ❜❡ ♦♥•② ❛•❣❡❜r❛✐❝✱ ❛ ❝❛s❡ s✐♠♣•❡r t❤❛♥ t❤❡ ❣❡♥❡r❛• ♦♥❡ ✇❤❡r❡ ♣❛tt❡r♥ ♠❛② ❝♦♥t❛✐♥ ❛❜str❛❝t✐♦♥s ✭s❡❡ ❬✶✹(✮✳ ❉❡✜♥✐t✐♦♥ ✶ ✭❙②♥t❛①✮✳ ❲❡ ❝♦♥s✐❞❡r t❤❡ s②♠❜♦•s ✏ ❴ ❴✑ ✭❛❜str❛❝t✐♦♥ ♦♣❡r❛t♦r✮✱ ✏ ❴ ≀ ❴✑ ✭str✉❝t✉r❡ ♦♣❡r❛t♦r✮✱ t❤❡ ✭❤✐❞❞❡♥✮ ❛♣♣•✐❝❛t✐♦♥ ♦♣❡r❛t♦r✱ ❛ s❡t X ♦❢ ✈❛r✐❛❜•❡s ❛♥❞ ❛ s❡t K ♦❢ ❝♦♥st❛♥ts✱ ❡❛❝❤ ♦❢ t❤❡♠ ❤❛✈✐♥❣ ❛♥ ❛r✐t② ❞❡♥♦t❡❞ ar(K)✳ ❚❤❡ s②♥t❛① ♦❢ t❤❡ ❜❛s✐❝ r❡✇r✐t✐♥❣ ❝❛•❝✉•✉s ✐s t❤❡ ❢♦••♦✇✐♥❣✿ T ::= X | K | P T | T T | T ≀ T ❚❡r♠s P ::= X | (. . . ((K P 1 ) P 2 ) . . . P ar(K) ❆•❣❡❜r❛✐❝ P❛tt❡r♥s ❆ •✐♥❡❛r ♣❛tt❡r♥ ✐s ❛ ♣❛tt❡r♥ ✇❤❡r❡ ❡✈❡r② ✈❛r✐❛❜•❡ ♦❝❝✉rs ❛t ♠♦st ♦♥❝❡✳ ❲❡ ❛ss✉♠❡ t❤❛t t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦♣❡r❛t♦r ❛ss♦❝✐❛t❡s t♦ t❤❡ •❡❢t✱ ✇❤✐•❡ t❤❡ ♦t❤❡r ♦♣❡r❛t♦rs ❛ss♦❝✐❛t❡ t♦ t❤❡ r✐❣❤t✳ ❚❤❡ ♣r✐♦r✐t② ♦❢ t❤❡ ❛♣♣•✐❝❛t✐♦♥ ✐s ❤✐❣❤❡r t❤❛♥ t❤❛t ♦❢ ✏ ❴ ❴✑ ✇❤✐❝❤ ✐s✱ ✐♥ t✉r♥✱ ♦❢ ❤✐❣❤❡r ♣r✐♦r✐t② t❤❛♥ t❤❡ ✏ ❴ ≀ ❴✑✳ ■♥ t❤❡ ❢♦••♦✇✐♥❣✱ t❤❡ s②♠❜♦•s A, B, C, . . . r❛♥❣❡ ♦✈❡r t❤❡ s❡t T ♦❢ t❡r♠s✱ t❤❡ s②♠❜♦•s x, y, z, . . . r❛♥❣❡ ♦✈❡r t❤❡ s❡t X ♦❢ ✈❛r✐❛❜•❡s ✭X ⊆ T ✮✱ t❤❡ s②♠❜♦•s a, b, c, . . . , f, g, h, . . . ❛♥❞ str✐♥❣s ❜✉✐•t ❢r♦♠ t❤❡♠ r❛♥❣❡ ♦✈❡r ❛ s❡t K ♦❢ ❝♦♥st❛♥ts ✭K ⊆ T ✮✳ ❋✐♥❛••②✱ t❤❡ s②♠❜♦•s P, Q r❛♥❣❡ ♦✈❡r t❤❡ s❡t P ♦❢ ♣❛tt❡r♥s✱ ✭X ⊆ P ⊆ T ✮✳ ❱❡❝t♦rs ♦❢ t❡r♠s (A 1 , . . . , A n ) ❛r❡ ❞❡♥♦t❡❞ ❜② A✳ ❲❡ ✉s✉❛••② ❞❡♥♦t❡ ❛ t❡r♠ ♦❢ t❤❡ ❢♦r♠ (. . . ((f A 1 ) A 2 ) . . . A n ) ❜② f (A 1 , A 2 , . . . , A n )✳ ■❞❡♥t✐t② ♦❢ t❡r♠s ✐s ❞❡♥♦t❡❞ ❜② ≡✳ ❆ t❡r♠ ♦❢ t❤❡ ❢♦r♠ P B ✐s ❛♥ ❛❜str❛❝t✐♦♥ ✭♦r r✉•❡✮ ✇✐t❤ ♣❛tt❡r♥ P ❛♥❞ ❜♦❞② B❀ ✐♥t✉✐t✐✈❡•②✱ t❤❡ ❢r❡❡ ✈❛r✐❛❜•❡s ♦❢ P ❛r❡ ❜♦✉♥❞ ✐♥ B✳ ❚❤❡ t❡r♠ A ≀ B ✐s ❝❛••❡❞ ❛ str✉❝t✉r❡✳ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✾ ❆s ❢♦r t❤❡ •❛♠❜❞❛✲❝❛•❝✉•✉s ❢♦r ✐♥st❛♥❝❡✱ t❤❡ r❡❞✉❝t✐♦♥ r❡•❛t✐♦♥ → → ♦❢ t❤❡ r❡✇r✐t✐♥❣ ❝❛•❝✉•✉s ✐s ❞❡✜♥❡❞ ❛s t❤❡ s♠❛••❡st ❝♦♥❣r✉❡♥❝❡ ❣❡♥❡r❛t❡❞ ❜② t❤❡ ❢♦••♦✇✐♥❣ t♦♣✲•❡✈❡• r❡❞✉❝t✐♦♥s✿ (P A) B → ρ Aθ if ∃θ. P θ ≡ B (A ≀ B) C → δ A C ≀ B C ❚❤❡ ♦♥❡ st❡♣ r❡❞✉❝t✐♦♥ r❡•❛t✐♦♥ ✐s ❞❡♥♦t❡❞ ❜② → ρ ♦r → δ ❛❝❝♦r❞✐♥❣ t♦ t❤❡ r❡❞✉❝t✐♦♥ r✉•❡ ✇❤✐❝❤ ✐s ✉s❡❞✳ ◆♦t✐❝❡ t❤❛t ✐♥ t❤❡ ♠❛✐♥ r❡❞✉❝t✐♦♥ ✭→ ρ ✮✱ t❤❡ ❝♦♥❞✐t✐♦♥ ❝♦♥s✐sts ✐♥ ❝❤❡❝❦✐♥❣ t❤❡ ❡①✐st❡♥❝❡ ♦❢ ❛ ♠❛t❝❤✐♥❣ s✉❜st✐t✉t✐♦♥ θ✳ ❲❤❡♥ ✐t ❡①✐sts✱ t❤✐s s✉❜st✐t✉t✐♦♥ ✐s ❛♣♣•✐❡❞ t♦ A✱ t❛❦✐♥❣ ❝❛r❡ ♦❢ ❢r❡❡ ❛♥❞ ❜♦✉♥❞❡❞ ✈❛r✐❛❜•❡s ❛s ✉s✉❛• ✐♥ ❛ ❤✐❣❤❡r✲♦r❞❡r s❡tt✐♥❣ ✭r❡♠❡♠❜❡r t❤❛t ✐s ❛♥ ❛❜str❛❝t♦r✮✳ ✺ ❙tr❛t❡❣✐❝ r❡❞✉❝t✐♦♥ ▲❡t ✉s ♥♦✇ ❝♦♠❡ ❜❛❝❦ t♦ t❤❡ ♠♦r❡ ❝•❛ss✐❝❛• ❝♦♥t❡①t ♦❢ ✜rst✲♦r❞❡r t❡r♠s ❛♥❞ t❡r♠ r❡✇r✐t✐♥❣ t♦ s❡❡ ❤♦✇ ✐t ✜ts t♦ t❤❡ ❣❡♥❡r❛• ♥♦t✐♦♥s ♣r❡s❡♥t❡❞ ❛❜♦✈❡✳ ❇❛s✐❝ ❞❡✜♥✐t✐♦♥s ♦♥ t❡r♠ r❡✇r✐t✐♥❣ ❝❛♥ ❜❡ ❢♦✉♥❞ ✐♥ ❬✸✸✱ ✸✼✱ ✺(✳ ❚❤❡ ❢♦••♦✇✐♥❣ st❛♥❞❛r❞ ♥♦t❛t✐♦♥s ✇✐•• ❜❡ ✉s❡❞ ✐♥ t❤❡ ❢♦••♦✇✐♥❣✳ T (F, X ) ✐s t❤❡ s❡t ♦❢ ✜rst✲♦r❞❡r t❡r♠s ❜✉✐•t ❢r♦♠ ❛ ❣✐✈❡♥ ✜♥✐t❡ s❡t F ♦❢ ❢✉♥❝t✐♦♥ s②♠❜♦•s ❛♥❞ ❛ ❞❡♥✉♠❡r❛❜•❡ s❡t X ♦❢ ✈❛r✐❛❜•❡s✳ ❚❤❡ s❡t ♦❢ ✈❛r✐❛❜•❡s ♦❝❝✉rr✐♥❣ ✐♥ ❛ t❡r♠ t ✐s ❞❡♥♦t❡❞ ❜② Var(t)✳ ■❢ Var(t) ✐s ❡♠♣t②✱ t ✐s ❝❛••❡❞ ❛ ❣r♦✉♥❞ t❡r♠ ❛♥❞ T (F) ✐s t❤❡ s❡t ♦❢ ❣r♦✉♥❞ t❡r♠s✳ ❆ s✉❜st✐t✉t✐♦♥ σ ✐s ❛♥ ❛ss✐❣♥♠❡♥t ❢r♦♠ X t♦ T (F, X )✱ ✇✐t❤ ❛ ✜♥✐t❡ ❞♦♠❛✐♥ {x 1 , . . . , x k } ❛♥❞ ✐s ✇r✐tt❡♥ σ = {x 1 → t 1 , . . . , x k → t k }✳ ✺✳✶ ❚❡r♠ r❡✇r✐t✐♥❣ ❆ r❡✇r✐t❡ r✉•❡ ✐s ❛♥ ♦r❞❡r❡❞ ♣❛✐r ♦❢ t❡r♠s l, r ∈ T (F, X )✱ ❞❡♥♦t❡❞ l → r✱ ✇❤❡r❡ ✐t ✐s ♦❢t❡♥ r❡q✉✐r❡❞ t❤❛t l ✐s ♥♦t ❛ ✈❛r✐❛❜•❡ ❛♥❞ Var(r) ⊆ Var(l)✳ ❲❡ ✇✐•• ❞r♦♣ t❤❡s❡ r❡str✐❝t✐♦♥s •❛t❡r✳ ❚❤❡ t❡r♠s l ❛♥❞ r ❛r❡ r❡s♣❡❝t✐✈❡•② ❝❛••❡❞ t❤❡ •❡❢t✲❤❛♥❞ s✐❞❡ ❛♥❞ t❤❡ r✐❣❤t✲❤❛♥❞ s✐❞❡ ♦❢ t❤❡ r✉•❡✳ ❆ r❡✇r✐t❡ s②st❡♠ ✐s ❛ ✭✜♥✐t❡ ♦r ✐♥✜♥✐t❡✮ s❡t ♦❢ r❡✇r✐t❡ r✉•❡s✳ |✉•❡s ❝❛♥ ❜❡ •❛❜❡••❡❞ t♦ ❡❛s✐•② t❛•❦ ❛❜♦✉t t❤❡♠✳ ❉❊❋■◆■❚■❖◆ ✶✹ ✭❖♥❡ st❡♣ r❡✇r✐t✐♥❣✮✳ •✐✈❡♥ ❛ r❡✇r✐t❡ s②st❡♠ R✱ ❛♥ ❛•✲ ❣❡❜r❛✐❝ t❡r♠ t ✐♥ T (F, X ) r❡✇r✐t❡s t♦ ❛♥ ❛•❣❡❜r❛✐❝ t❡r♠ t ′ ✐❢ t❤❡r❡ ❡①✐sts ❛ r❡✇r✐t❡ r✉•❡ l → r ♦❢ R ❛♥❞ ❛ ♣♦s✐t✐♦♥ ω ✐♥ t✱ s✉❝❤ t❤❛t ✐♥ t❤❡ ρ✲❝❛•❝✉•✉s✱ ❛♣♣•②✐♥❣ t❤❡ ρ✲t❡r♠ (l r) t♦ t ❛t ♣♦s✐t✐♦♥ ω ❡✈❛•✉❛t❡s t♦ t ′ ✱ ✇❤✐❝❤ ✐s ❞❡♥♦t❡❞ ❜② t[(l r)t |ω ] ω → ρ t ′ ❚❤✐s ✐s ❞❡♥♦t❡❞ t -→ l→r ω t ′ ♦r t -→ R ω t ′ ✇❤❡♥ ✇❡ ❞♦ ♥♦t ♥❡❡❞ t♦ ♠❛❦❡ ♣r❡❝✐s❡ ✇❤✐❝❤ r❡✇r✐t❡ r✉•❡ ✐s ✉s❡❞✳ ■♥❞❡❡❞ t❤✐s ♠❡❛♥s t❤❛t t❤❡r❡ ❡①✐sts ❛ s✉❜st✐t✉t✐♦♥ σ s✉❝❤ t❤❛t t |ω = σ(l) ❛♥❞ t ′ = t[σ(r)] ω ✳ ❆ s✉❜t❡r♠ t |ω ✇❤❡r❡ t❤❡ r❡✇r✐t✐♥❣ st❡♣ ✐s ❛♣♣•✐❡❞ ✐s ❝❛••❡❞ r❡❞❡①✳ ❆ t❡r♠ t❤❛t ❤❛s ♥♦ r❡❞❡① ✐s s❛✐❞ t♦ ❜❡ ✐rr❡❞✉❝✐❜•❡ ❢♦r R ♦r t♦ ❜❡ ✐♥ R✲♥♦r♠❛• ❢♦r♠✳ ❚♦ ❛ s❡t ♦❢ r❡✇r✐t❡ r✉•❡s ❝♦rr❡s♣♦♥❞s ❞✐r❡❝t•② ❛ ✉♥✐q✉❡ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ t❤❛t ❝❛♥ ❜❡ s❡❡♥ ❛s ❛ ❣❡♥❡r✐❝ ✇❛② t♦ ❞❡s❝r✐❜❡ t❤❡ s❡t ♦❢ ❛•• ❞❡r✐✈❛t✐♦♥s✳ ❉❊❋■◆■❚■❖◆ ✶✺ ✭|❡❞✉❝t✐♦♥ s②st❡♠✮✳ •✐✈❡♥ ❛ s❡t ♦❢ t❡r♠s T (F, X ) ❛♥❞ ❛ s❡t ♦❢ r❡✇r✐t❡ r✉•❡s R✱ ❛ r❡❞✉❝t✐♦♥ s②st❡♠ ✐s ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ R = (O R , S R ) ✇✐t❤✿ • O R = T (F, X )✱ ❛♥❞ • S R = {t → t ′ |t -→ R ω t ′ ❢♦r ω ❛ ♣♦s✐t✐♦♥ ✐♥ t}✳ ■t ✐s ♥♦✇ ♣♦ss✐❜•❡ t♦ ❣✐✈❡ t❤❡ ❞❡✜♥✐t✐♦♥ ♦❢ str❛t❡❣✐❝ r❡✇r✐t✐♥❣✿ ❉❊❋■◆■❚■❖◆ ✶✻ ✭❙tr❛t❡❣✐❝ r❡✇r✐t✐♥❣✮✳ •✐✈❡♥ ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ R = (O R , S R ) ❣❡♥❡r❛t❡❞ ❜② ❛ t❡r♠ r❡✇r✐t❡ s②st❡♠ R✱ ❛♥❞ ❛ str❛t❡❣② ζ ♦❢ R✱ ❛ str❛t❡❣✐❝ r❡✇r✐t✐♥❣ ❞❡r✐✈❛t✐♦♥ ✭♦r r❡✇r✐t✐♥❣ ❞❡r✐✈❛t✐♦♥ ✉♥❞❡r str❛t❡❣② ζ✮ ✐s ❛♥ ❡•❡♠❡♥t ♦❢ ζ✳ ❆ str❛t❡❣✐❝ r❡✇r✐t✐♥❣ st❡♣ ✉♥❞❡r ζ ✐s ❛ r❡✇r✐t✐♥❣ st❡♣ t -→ R ω t ′ t❤❛t ♦❝❝✉rs ✐♥ ❛ ❞❡r✐✈❛t✐♦♥ ♦❢ ζ✳ ◆♦t✐❝❡ t❤❛t t❤❡ ♣r❡✈✐♦✉s ❞❡✜♥✐t✐♦♥s ❡①t❡♥❞ ✐♠♠❡❞✐❛t•② t♦ t❤❡ ❝❛s❡ ✇❤❡r❡ ♠❛t❝❤✐♥❣ ✐s ♣❡r❢♦r♠❡❞ ♠♦❞✉•♦ ❛♥ ❡q✉❛t✐♦♥❛• t❤❡♦r② •✐❦❡ ❛ss♦❝✐❛t✐✈✐t②✲ ❝♦♠♠✉t❛t✐✈✐t② ♦❢ s♦♠❡ ❢♦♥❝t✐♦♥ s②♠❜♦•s✳ ❙tr❛t❡❣✐❝ r❡✇r✐t✐♥❣ ❝❛♥ t❤❡r❡❢♦r❡ ❜❡ ❞❡✜♥❡❞ ❢♦r r❡✇r✐t✐♥❣ ♠♦❞✉•♦ r❡•❛t✐♦♥s ❛s ❞❡✜♥❡❞ ✐♥ ❬✺✶✱ ✸✶(✳ ❇❡s✐❞❡s t❤❡ r❡✇r✐t✐♥❣ r❡•❛t✐♦♥✱ ❛♥♦t❤❡r r❡❞✉❝t✐♦♥ r❡•❛t✐♦♥✱ ❝❛••❡❞ ♥❛r✲ r♦✇✐♥❣✱ ✐s ✇♦rt❤ ❝♦♥s✐❞❡r✐♥❣ t♦ ❞❡✈❡•♦♣ ❛♥ ❆|❙✳ ❚❤✐s ✇❡••✲❦♥♦✇♥ ♣r♦❝❡ss✱ ✐♥tr♦❞✉❝❡❞ ✐♥ ❬✷✷✱ ✷✾(✱ ✐s q✉✐t❡ s✐♠✐•❛r t♦ r❡✇r✐t✐♥❣ ❜✉t t❤❡r❡✱ ♠❛t❝❤✐♥❣ ✐s r❡♣•❛❝❡❞ ❜② ✉♥✐✜❝❛t✐♦♥✳ ▲❡t ✉s r❡❝❛•• ✐ts ✉s✉❛• ❞❡✜♥✐t✐♦♥✿ ❉❊❋■◆■❚■❖◆ ✶✼ ✭❖♥❡ st❡♣ ♥❛rr♦✇✐♥❣✮✳ •✐✈❡♥ ❛ t❡r♠ r❡✇r✐t❡ s②st❡♠ R✱ ❛♥ ❛•❣❡❜r❛✐❝ t❡r♠ t ✐♥ T (F, X ) ♥❛rr♦✇s t♦ ❛♥ ❛•❣❡❜r❛✐❝ t❡r♠ t ′ ✐❢ t❤❡r❡ ❡①✐sts ❛ r❡✇r✐t❡ r✉•❡ l → r ♦❢ R ❛♥❞ ❛ ♣♦s✐t✐♦♥ ω ✐♥ t✱ s✉❝❤ t❤❛t t| ω ❛♥❞ l ❛r❡ ✉♥✐✜❛❜•❡ ✇✐t❤ ❛ ♠♦st ❣❡♥❡r❛• ✉♥✐✜❡r σ✳ ❚❤❡♥ t ′ = σ(t[r] ω )✳ ❚❤✐s ✐s ❞❡♥♦t❡❞ t l→r ω,σ t ′ ✇❤❡r❡ ❡✐t❤❡r ω ♦r σ ♠❛② ❜❡ ♦♠✐tt❡❞✱ ♦r s✐♠♣•② t R t ′ ✇❤❡♥ ✇❡ ❞♦ ♥♦t ♥❡❡❞ t♦ ♠❛❦❡ ♣r❡❝✐s❡ ✇❤✐❝❤ r❡✇r✐t❡ r✉•❡ ✐s ✉s❡❞✳ ❋♦r ✐♥st❛♥❝❡✱ ✉s✐♥❣ t❤❡ r❡✇r✐t❡ r✉•❡ f (x, x) → x t❤❡ t❡r♠ f (g(y), z) ♥❛r✲ r♦✇s t♦ t❤❡ t❡r♠ g(y) ✇✐t❤ t❤❡ s✉❜st✐t✉t✐♦♥ σ = {x → g(y), z → g(y)}✳ ❚❤❡♥✱ ✇❡ ❝❛♥ ❛•s♦ ❝♦♥s✐❞❡r t❤❛t ❛ r❡✇r✐t❡ s②st❡♠ R ❣❡♥❡r❛t❡s ✐♥ ❛ s✐♠✐•❛r ✇❛② ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ N = (O R , S R ) ✇✐t❤✿ • O R = T (F, X )✱ ❛♥❞ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✶✶ • S R = {t t ′ |t l→r ω t ′ ❢♦r ω ❛ ♣♦s✐t✐♦♥ ✐♥ t}✳ ❆s ❢♦r t❤❡ r❡✇r✐t✐♥❣ r❡•❛t✐♦♥✱ ✇❡ ✇✐•• t❤❡r❡❢♦r❡ ✉s❡ t❤❡ ❞❡✜♥✐t✐♦♥s ❣✐✈❡♥ ✐♥ t❤❡ ❛❜str❛❝t s❡tt✐♥❣ ❛♥❞ ✇❡ ❝❛♥ ❞❡✜♥❡ str❛t❡❣✐❝ ♥❛rr♦✇✐♥❣✿ ❉❊❋■◆■❚■❖◆ ✶✽ ✭❙tr❛t❡❣✐❝ ♥❛rr♦✇✐♥❣✮✳ •✐✈❡♥ ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ N = (O R , S R ) ❣❡♥❡r❛t❡❞ ❜② ❛ t❡r♠ r❡✇r✐t❡ s②st❡♠ R✱ ❛♥❞ ❛ str❛t❡❣② ζ ♦❢ N ✱ ❛ str❛t❡❣✐❝ ♥❛rr♦✇✐♥❣ ❞❡r✐✈❛t✐♦♥ ✭♦r ♥❛rr♦✇✐♥❣ ❞❡r✐✈❛t✐♦♥ ✉♥❞❡r str❛t❡❣② ζ✮ ✐s ❛♥ ❡•❡♠❡♥t ♦❢ ζ✳ ❆ str❛t❡✲ ❣✐❝ ♥❛rr♦✇✐♥❣ st❡♣ ✉♥❞❡r ζ ✐s ❛ ♥❛rr♦✇✐♥❣ st❡♣ t R ω t ′ t❤❛t ♦❝❝✉rs ✐♥ ❛ ❞❡r✐✈❛t✐♦♥ ♦❢ ζ✳ ✺✳✷ ❚❡r♠ r❡✇r✐t✐♥❣ str❛t❡❣✐❡s ■♥ t❤❡ ❝•❛ss✐❝❛• s❡tt✐♥❣ ♦❢ ✜rst✲♦r❞❡r t❡r♠ r❡✇r✐t✐♥❣✱ str❛t❡❣✐❡s ❤❛✈❡ ❜❡❡♥ ✉s❡❞ t♦ ❞❡t❡r♠✐♥❡ ❛t ❡❛❝❤ st❡♣ ♦❢ ❛ ❞❡r✐✈❛t✐♦♥ ✇❤✐❝❤ ✐s t❤❡ ♥❡①t r❡❞❡①✳ ❚❤✉s t❤❡② ❤❛✈❡ ♦❢t❡♥ ❜❡❡♥ ❞❡✜♥❡❞ ❛s ❢✉♥❝t✐♦♥s ♦♥ t❤❡ s❡t ♦❢ t❡r♠s •✐❦❡ ✐♥ ❬✺✹(✳ ■♥ ♦✉r ❣❡♥❡r❛• s❡tt✐♥❣ ♦❢ ❛❜str❛❝t str❛t❡❣✐❡s✱ t❤❡ ❞❡✜♥✐t✐♦♥s ♦❢ t❤❡s❡ st❛♥❞❛r❞ str❛t❡❣✐❡s ❡①♣r❡ss ❛ ♣r♦♣❡rt② t❤❛t ❛ ❞❡r✐✈❛t✐♦♥ ♠✉st s❛t✐s❢② t♦ ❜❡•♦♥❣ t♦ t❤❡ str❛t❡❣② ♦❢ ✐♥t❡r❡st✳ ▲❡t ✉s ✐••✉str❛t❡ t❤✐s ♣♦✐♥t ♦❢ ✈✐❡✇ ❜② ❛ ❢❡✇ ❡①❛♠♣•❡s ♦❢ str❛t❡❣✐❡s t❤❛t ❤❛✈❡ ❜❡❡♥ ♣r✐♠❛r✐•② ♣r♦✈✐❞❡❞ t♦ ❞❡s❝r✐❜❡ t❤❡ ♦♣❡r❛t✐♦♥❛• s❡♠❛♥t✐❝s ♦❢ ❢✉♥❝t✐♦♥❛• ♣r♦❣r❛♠♠✐♥❣ •❛♥❣✉❛❣❡s ❛♥❞ t❤❡ r❡•❛t❡❞ ♥♦t✐♦♥s ♦❢ ❝❛•• ❜② ✈❛•✉❡✱ ❝❛•• ❜② ♥❛♠❡✱ ❝❛•• ❜② ♥❡❡❞✳ ▲❡❢t♠♦st✲✐♥♥❡r♠♦st ❛♥❞ ♦✉t❡r♠♦st r❡❞✉❝t✐♦♥ ▲❡t R ❜❡ ❛ r❡✇r✐t❡ s②st❡♠ ♦♥ T (F, X )✳ ❆ r❡✇r✐t✐♥❣ ❞❡r✐✈❛t✐♦♥ ✉♥❞❡r t❤❡ ✐♥♥❡r♠♦st ✭r❡s♣✳ ♦✉t❡r♠♦st✮ str❛t❡❣② ✈❡r✐✜❡s ✿ ❢♦r ❛ ❣✐✈❡♥ t❡r♠ t ∈ T (F, X )✱ t → R ω t ′ ❛♥❞ t❤❡ r❡✇r✐t✐♥❣ ♣♦s✐t✐♦♥ ω ✐♥ t ✐s s✉❝❤ t❤❛t t❤❡r❡ ✐s ♥♦ s✉✣① ✭r❡s♣✳ ♣r❡✜①✮ ♣♦s✐t✐♦♥ ω ′ ♦❢ ω s✉❝❤ t❤❛t t r❡✇r✐t❡s ❛t ♣♦s✐t✐♦♥ ω ′ ✳ ▲❛③② r❡❞✉❝t✐♦♥ ▲❛③② r❡❞✉❝t✐♦♥✱ ❛s ♣❡r❢♦r♠❡❞ ✐♥ ❍❛s❦❡•• ❢♦r ✐♥st❛♥❝❡✱ ♦r ❞❡s❝r✐❜❡❞ ✐♥ ❬✷✸(✱ ❝♦♠❜✐♥❡s ✐♥♥❡r♠♦st ❛♥❞ ♦✉t❡r♠♦st str❛t❡❣✐❡s✱ ✐♥ ♦r❞❡r t♦ ❛✈♦✐❞ r❡❞✉♥❞❛♥t r❡✇r✐t❡ st❡♣s✳ ❋♦r t❤❛t✱ ♦♣❡r❛t♦rs ♦❢ t❤❡ s✐❣♥❛t✉r❡ ❤❛✈❡ •❛❜❡•s s♣❡❝✐❢②✐♥❣ ✇❤✐❝❤ ❛r❣✉♠❡♥ts ❛r❡ •❛③② ♦r ❡❛❣❡r✳ P♦s✐t✐♦♥s ✐♥ t❡r♠s ❛r❡ t❤❡♥ ❛♥♥♦t❛t❡❞ ❛s •❛③② ♦r ❡❛❣❡r✱ ❛♥❞ t❤❡ str❛t❡❣② ❝♦♥s✐sts ✐♥ r❡❞✉❝✐♥❣ t❤❡ ❡❛❣❡r s✉❜t❡r♠s ♦♥•② ✇❤❡♥ t❤❡✐r r❡❞✉❝t✐♦♥ ❛••♦✇s ❛ r❡❞✉❝t✐♦♥ st❡♣ ❤✐❣❤❡r ✐♥ t❤❡ t❡r♠ ❬✹✽(✳ ▲❛③② r❡❞✉❝t✐♦♥ ❝❛♥ ❛•s♦ ❜❡ ♣❡r❢♦r♠❡❞ ✇✐t❤ ♦t❤❡r ♠❡❝❤❛♥✐s♠s✱ s✉❝❤ ❛s •♦❝❛• str❛t❡❣✐❡s ♦r ❝♦♥t❡①t✲s❡♥s✐t✐✈❡ r❡✇r✐t✐♥❣✳ |❡❞✉❝t✐♦♥ ✉♥❞❡r •♦❝❛• str❛t❡❣✐❡s ▲♦❝❛• str❛t❡❣✐❡s ♦♥ ♦♣❡r❛t♦rs✱ ✉s❡❞ ❢♦r ✐♥st❛♥❝❡ ✐♥ t❤❡ ❖❇❏✲•✐❦❡ •❛♥✲ ❣✉❛❣❡s ❬✷✺(✱ ✐♥tr♦❞✉❝❡ ❛ ❢✉♥❝t✐♦♥ LS ❢r♦♠ F t♦ t❤❡ s❡t L(N) ♦❢ •✐sts ♦❢ ✐♥t❡❣❡rs t♦ s♣❡❝✐❢② ✇❤✐❝❤ ❛♥❞ ✐♥ ✇❤✐❝❤ ♦r❞❡r t❤❡ ❛r❣✉♠❡♥ts ♦❢ ❡❛❝❤ ❢✉♥❝t✐♦♥ s②♠❜♦• ❤❛✈❡ t♦ ❜❡ r❡❞✉❝❡❞✳ ❆t ❡❛❝❤ st❡♣ ♦❢ t❤❡ ❞❡r✐✈❛t✐♦♥✱ ❢♦r t❤❡ ❝✉rr❡♥t t❡r♠ t✱ t❤❡ ♥❡①t r❡❞❡① ✐s ❝❤♦s❡♥ ❛❝❝♦r❞✐♥❣ t♦ LS (f ) ✇❤❡r❡ f ✐s t❤❡ t♦♣ ♦♣❡r❛t♦r ♦❢ t❤❡ t❡r♠ t✳ ❈♦♥t❡①t✲s❡♥s✐t✐✈❡ r❡❞✉❝t✐♦♥ ▲♦❝❛• str❛t❡❣✐❡s ❛r❡ ❝•♦s❡ t♦ ❝♦♥t❡①t✲s❡♥s✐t✐✈❡ r❡✇r✐t✐♥❣ ❬✹✶✱ ✹✷✱ ✶(✱ ✇❤❡r❡ r❡✇r✐t✐♥❣ ✐s ❛•s♦ ❛••♦✇❡❞ ♦♥•② ❛t s♦♠❡ s♣❡❝✐✜❡❞ ♣♦s✐t✐♦♥s ✐♥ t❤❡ t❡r♠s✳ ❚❤❡ ❢♦r♠❡r s♣❡❝✐❢② ❛♥ ♦r❞❡r✐♥❣ ♦♥ t❤❡s❡ r❡✇r✐t✐♥❣ ♣♦s✐t✐♦♥s✱ s♦ t❤❡② ❛r❡ ♠♦r❡ s♣❡❝✐✜❝ t❤❛♥ ❝♦♥t❡①t✲s❡♥s✐t✐✈❡ r❡✇r✐t✐♥❣ ✇❤❡r❡ ❛ r❡❞❡① ✐s ❝❤♦s❡♥ ✐♥ ❛ s❡t ♦❢ ♣♦s✐t✐♦♥s✳ ▼♦r❡ ♣r❡❝✐s•❡②✱ ❤❡r❡✱ ❛ r❡♣•❛❝❡♠❡♥t ♠❛♣ ✐s ❛ ♠❛♣♣✐♥❣ µ : F → P(N) s❛t✐s❢②✐♥❣ µ(f ) ⊆ {1, . . . , k}✱ ❢♦r ❡❛❝❤ k✲❛r② s②♠❜♦• f ♦❢ ❛ s✐❣♥❛t✉r❡ F ❬✹✵(✳ |❡♣•❛❝❡♠❡♥t ♠❛♣s ❞✐s❝r✐♠✐♥❛t❡ t❤❡ ❛r❣✉♠❡♥t ♣♦s✐t✐♦♥s ♦♥ ✇❤✐❝❤ t❤❡ r❡✇r✐t✐♥❣ st❡♣s ❛r❡ ❛••♦✇❡❞✳ ◆❡❡❞❡❞ ❛♥❞ st❛♥❞❛r❞ r❡❞✉❝t✐♦♥ ■♥ ❬✷✼✱ ✷✽(✱ t❤❡ ♥♦t✐♦♥s ♦❢ ♥❡❡❞❡❞ ❛♥❞ str♦♥❣•② ♥❡❡❞❡❞ r❡❞❡①❡s ❛r❡ ❞❡✜♥❡❞ ❢♦r ♦rt❤♦❣♦♥❛• r❡✇r✐t❡ s②st❡♠s✳ ❚❤❡ ♠❛✐♥ ✐❞❡❛ ❤❡r❡ ✐s t♦ ✜♥❞ t❤❡ ♦♣t✐♠❛• ✇❛②✱ ✇❤❡♥ ✐t ❡①✐sts✱ t♦ r❡❛❝❤ t❤❡ ♥♦r♠❛• ❢♦r♠ ❛ t❡r♠✳ ❆ r❡❞❡① ✐s ♥❡❡❞❡❞ ✇❤❡♥ t❤❡r❡ ✐s ♥♦ ✇❛② t♦ ❛✈♦✐❞ r❡❞✉❝✐♥❣ ✐t t♦ r❡❛❝❤ t❤❡ ♥♦r♠❛• ❢♦r♠✳ |❡❞✉❝✐♥❣ ♦♥•② ♥❡❡❞❡❞ r❡❞❡①❡s ✐s ❝•❡❛r•② t❤❡ ♦♣t✐♠❛• r❡❞✉❝t✐♦♥ str❛t❡❣②✱ ❛s s♦♦♥ ❛s ♥❡❡❞❡❞ r❡❞❡①❡s ❝❛♥ ❜❡ ❞❡❝✐❞❡❞✱ ✇❤✐❝❤ ✐s ♥♦t t❤❡ ❝❛s❡ ✐♥ ❣❡♥❡r❛•✳ ✺✳✸ ❙tr❛t❡❣② •❛♥❣✉❛❣❡ ❢♦r r❡❞✉❝t✐♦♥ ❚❤✐s s❡❝t✐♦♥ ✐s ❞❡✈♦t❡❞ t♦ ❡①♣r❡ss✐♥❣ r❡✇r✐t✐♥❣ str❛t❡❣✐❡s❀ ❡①❛❝t•② t❤❡ s❛♠❡ ♣r✐♥❝✐♣•❡s ❝♦✉•❞ ❜❡ ✉s❡❞ t♦ ❡①♣r❡ss ♦t❤❡r str❛t❡❣✐❡s ❛s ✇❡ ✇✐•• s❡❡ •❛t❡r✳ ■♥ t❤❡ ✶✾✾✵s✱ ❣❡♥❡r❛•✐③✐♥❣ ❖❇❏✬s ❝♦♥❝❡♣t ♦❢ •♦❝❛• str❛t❡❣✐❡s✱ t❤❡ ✐❞❡❛ ❤❛s ❡♠❡r❣❡❞ t♦ ❜❡tt❡r ❢♦r♠❛•✐③❡ t❤❡ ❝♦♥tr♦• ♦♥ r❡✇r✐t✐♥❣ ✇❤✐❝❤ ✇❛s ♣❡r❢♦r♠❡❞ ✐♠♣•✐❝✐t•② ✐♥ ✐♥t❡r♣r❡t❡rs ♦r ❝♦♠♣✐•❡rs ♦❢ r✉•❡✲❜❛s❡❞ ♣r♦❣r❛♠♠✐♥❣ •❛♥❣✉❛❣❡s✳ ❚❤❡♥ ✐♥st❡❛❞ ♦❢ ❞❡s❝r✐❜✐♥❣ ❛ str❛t❡❣② ❜② ❛ ♣r♦♣❡rt② ♦❢ ✐ts ❞❡r✐✈❛t✐♦♥s✱ t❤❡ ✐❞❡❛ ✐s ♥♦✇ t♦ ♣r♦✈✐❞❡ ❛ str❛t❡❣② •❛♥❣✉❛❣❡ t♦ s♣❡❝✐❢② ✇❤✐❝❤ ❞❡r✐✈❛t✐♦♥s ✇❡ ❛r❡ ✐♥t❡r❡st❡❞ ✐♥✳ ❱❛r✐♦✉s ❛♣♣r♦❛❝❤❡s ❤❛✈❡ ❢♦••♦✇❡❞✱ ②✐❡•❞✐♥❣ ❞✐✛❡r❡♥t str❛t❡❣② •❛♥❣✉❛❣❡s s✉❝❤ ❛s ❊▲❆◆ ❬✸✹✱ ✶✵(✱ ❆P❙ ❬✸✾(✱ ❙tr❛t❡❣♦ ❬✺✻(✱ ❚❖▼ ❬✻( ♦r ♠♦r❡ r❡❝❡♥t•② ▼❛✉❞❡ ❬✹✹(✳ ❆•• t❤❡s❡ •❛♥❣✉❛❣❡s s❤❛r❡ t❤❡ ❝♦♥❝❡r♥ t♦ ♣r♦✈✐❞❡ ❛❜str❛❝t ✇❛②s t♦ ❡①♣r❡ss ❝♦♥tr♦• ♦❢ r✉•❡ ❛♣♣•✐❝❛t✐♦♥s✱ ❜② ✉s✐♥❣ r❡✢❡①✐✈✐t② ❛♥❞ t❤❡ ♠❡t❛✲ •❡✈❡• ❢♦r ▼❛✉❞❡✱ ♦r ❛ str❛t❡❣② •❛♥❣✉❛❣❡ ❢♦r ❊▲❆◆✱ ❙tr❛t❡❣♦ ♦r ❆❙❋✰❙❉❋✳ ❙tr❛t❡❣✐❡s s✉❝❤ ❛s ❜♦tt♦♠✲✉♣✱ t♦♣✲❞♦✇♥ ♦r •❡❢t♠♦st✲✐♥♥❡r♠♦st ❛r❡ ❤✐❣❤ •❡✈❡• ✇❛②s t♦ ❞❡s❝r✐❜❡ ❤♦✇ r❡✇r✐t❡ r✉•❡s s❤♦✉•❞ ❜❡ ❛♣♣•✐❡❞✳ ❚❖▼✱ ❊▲❆◆✱ ▼❛✉❞❡ ❛♥❞ ❙tr❛t❡❣♦ ♣r♦✈✐❞❡ ✢❡①✐❜•❡ ❛♥❞ ❡①♣r❡ss✐✈❡ str❛t❡❣② •❛♥❣✉❛❣❡s ✇❤❡r❡ ❤✐❣❤✲ •❡✈❡• str❛t❡❣✐❡s ❛r❡ ❞❡✜♥❡❞ ❜② ❝♦♠❜✐♥✐♥❣ •♦✇✲•❡✈❡• ♣r✐♠✐t✐✈❡s✳ ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ❝❤♦♦s❡ ❚❖▼ ❬✼( ✶ t♦ ✐••✉str❛t❡ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ str❛t❡❣② •❛♥❣✉❛❣❡s ♦❢ t❤✐s ❢❛♠✐•② ❛♥❞ ✇❡ ❞❡s❝r✐❜❡ ❜❡•♦✇ t❤❡ ♠❛✐♥ ❡•❡♠❡♥ts ♦❢ t❤❡ •❛♥❣✉❛❣❡✳ ❚❤❡ ✶ ❤tt♣✿✴✴t♦♠✳•♦r✐❛✳❢r ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✶✸ s❡♠❛♥t✐❝s ♦❢ t❤❡ ❚❖▼ str❛t❡❣② •❛♥❣✉❛❣❡ ❛s ✇❡•• ❛s ♦t❤❡rs ❛r❡ ♥❛t✉r❛••② ❞❡s❝r✐❜❡❞ ✐♥ t❤❡ r❡✇r✐t✐♥❣ ❝❛•❝✉•✉s ❬✶✹✱ ✶✺(✳ ❲❡ ❝❛♥ ❞✐st✐♥❣✉✐s❤ t✇♦ ❝•❛ss❡s ♦❢ ❝♦♥str✉❝ts ✐♥ t❤❡ str❛t❡❣② •❛♥❣✉❛❣❡✿ t❤❡ ✜rst ♦♥❡ ❛••♦✇s ❝♦♥str✉❝t✐♦♥ ♦❢ ❞❡r✐✈❛t✐♦♥s ❢r♦♠ t❤❡ ❜❛s✐❝ ❡•❡♠❡♥ts✱ ♥❛♠❡•② t❤❡ r❡✇r✐t❡ r✉•❡s✳ ❚❤❡ s❡❝♦♥❞ ♦♥❡ ❝♦rr❡s♣♦♥❞s t♦ ❝♦♥str✉❝ts t❤❛t ❡①♣r❡ss t❤❡ ❝♦♥tr♦•✱ ❡s♣❡❝✐❛••② ❞❡t❡r♠✐♥✐st✐❝ ❛♥❞ ✉♥❞❡t❡r♠✐♥✐st✐❝ ❝❤♦✐❝❡✳ ▼♦r❡♦✈❡r✱ t❤❡ ❝❛♣❛❜•✐•✐t② ♦❢ ❡①♣r❡ss✐♥❣ r❡❝✉rs✐♦♥ ✐♥ t❤❡ •❛♥❣✉❛❣❡ ❜r✐♥❣s ❡✈❡♥ ♠♦r❡ ❡①♣r❡ss✐✈❡ ♣♦✇❡r✳ ❊•❡♠❡♥t❛r② str❛t❡❣✐❡s ❆♥ ❡•❡♠❡♥t❛r② str❛t❡❣② ✐s ❡✐t❤❡r Identity ✇❤✐❝❤ ❝♦rr❡s♣♦♥❞s t♦ t❤❡ s❡t Id ♦❢ ❛•• ❡♠♣t② ❞❡r✐✈❛t✐♦♥s✱ F ail ✇❤✐❝❤ ❞❡♥♦t❡s t❤❡ ❡♠♣t② s❡t ♦❢ ❞❡r✐✈❛t✐♦♥s F ail✱ ♦r ❛ s❡t ♦❢ r❡✇r✐t❡ r✉•❡s R ✇❤✐❝❤ r❡♣r❡s❡♥ts ♦♥❡✲st❡♣ ❞❡r✐✈❛t✐♦♥s ✇✐t❤ r✉•❡s ✐♥ R ❛t t❤❡ r♦♦t ♣♦s✐t✐♦♥✳ Sequence(s 1 , s 2 )✱ ❛•s♦ ❞❡♥♦t❡❞ s 2 ; s 1 ✐s t❤❡ ❝♦♥❝❛t❡♥❛t✐♦♥ ♦❢ s 1 ❛♥❞ s 2 ✇❤❡♥❡✈❡r ✐t ❡①✐sts✿ Sequence(s 1 , s 2 )t = s 2 (s 1 t)✳ ❈♦♥tr♦• str❛t❡❣✐❡s ❆ ❢❡✇ ❝♦♥str✉❝t✐♦♥s ❛r❡ ♥❡❡❞❡❞ t♦ ❜✉✐•❞ ❞❡r✐✈❛t✐♦♥s✱ ❜r❛♥❝❤✐♥❣ ❛♥❞ t❛❦❡ ✐♥t♦ ❛❝❝♦✉♥t t❤❡ str✉❝t✉r❡ ♦❢ ❡•❡♠❡♥ts ✭t❡r♠s✮✳ ❝❤♦✐❝❡ Choice(s 1 , s 2 ) s❡•❡❝ts t❤❡ ✜rst str❛t❡❣② t❤❛t ❞♦❡s ♥♦t ❢❛✐•❀ ✐t ❢❛✐•s ✐❢ ❜♦t❤ ❢❛✐•✿ Choice(s 1 , s 2 )t = s 1 t ✐❢ s 1 t ❞♦❡s ♥♦t ❢❛✐• ❡•s❡ s 2 t✳ ❛•• s✉❜t❡r♠s ❖♥ ❛ t❡r♠ t✱ All(s) ❛♣♣•✐❡s t❤❡ str❛t❡❣② s ♦♥ ❛•• ✐♠♠❡❞✐❛t❡ s✉❜t❡r♠s✿ All(s)f (t 1 , ..., t n ) = f (t ′ 1 , ..., t ′ n ) ✐❢ st 1 = t ′ 1 , ..., st n = t ′ n ❀ ✐t ❢❛✐•s ✐❢ t❤❡r❡ ❡①✐sts i s✉❝❤ t❤❛t st i ❢❛✐•s✳ ♦♥❡ s✉❜t❡r♠ ❖♥ ❛ t❡r♠ t✱ One(s) ❛♣♣•✐❡s t❤❡ str❛t❡❣② s ♦♥ t❤❡ ✜rst ✐♠✲ ♠❡❞✐❛t❡ s✉❜t❡r♠ ✇❤❡r❡ s ❞♦❡s ♥♦t ❢❛✐•✿ One(s)f (t 1 , ..., t n ) = f (t 1 , ..., t ′ i , ..., t n ) ✐❢ ❢♦r ❛•• j < i✱ st j ❢❛✐•s✱ ❛♥❞ st i = t ′ i ❀ ✐t ❢❛✐•s ✐❢ ❢♦r ❛•• i✱ st i ❢❛✐•s✳ ✜①♣♦✐♥t ❚❤❡ µ r❡❝✉rs✐♦♥ ♦♣❡r❛t♦r ✭❝♦♠♣❛r❛❜•❡ t♦ rec ✐♥ ❖❈❛♠•✮ ✐s ✐♥tr♦✲ ❞✉❝❡❞ t♦ ❛••♦✇ t❤❡ r❡❝✉rs✐✈❡ ❞❡✜♥✐t✐♦♥ ♦❢ str❛t❡❣✐❡s✳ µx.s ❛♣♣•✐❡s t❤❡ ❞❡r✐✈❛t✐♦♥ ✐♥ s ✇✐t❤ t❤❡ ✈❛r✐❛❜•❡ x ✐♥st❛♥t✐❛t❡❞ ✇✐t❤ µx.s✿ µx.s = s[x ← µx.s] ❚❤❡s❡ str❛t❡❣✐❡s ❛r❡ t❤❡♥ ❝♦♠♣♦s❡❞ t♦ ❜✉✐•❞ ♠♦r❡ ❡•❛❜♦r❛t❡❞ ♦♥❡s✳ ❋♦r ✐♥st❛♥❝❡ T ry(s) = choice(s, Identity)✿ T ry(s) ❛♣♣•✐❡s s ✐❢ ✐t ❝❛♥✱ ❛♥❞ ♣❡r✲ ❢♦r♠s t❤❡ Identity ♦t❤❡r✇✐s❡✳ ❚❤❡ All ❛♥❞ One ❝♦♠❜✐♥❛t♦rs ❛r❡ ✉s❡❞ ✐♥ ❝♦♠❜✐♥❛t✐♦♥ ✇✐t❤ t❤❡ ✜①♣♦✐♥t ♦♣❡r❛t♦r t♦ ❞❡✜♥❡ tr❡❡ tr❛✈❡rs❛•s✳ ❋♦r ❡①❛♠✲ ♣•❡✱ ✇❡ ❤❛✈❡ T opDown(s) = µx.Sequence(s, All(x))✿ t❤❡ str❛t❡❣② s ✐s ✜rst ❛♣♣•✐❡❞ ♦♥ t♦♣ ♦❢ t❤❡ ❝♦♥s✐❞❡r❡❞ t❡r♠✱ t❤❡♥ t❤❡ str❛t❡❣② T opDown(s) ✐s r❡❝✉rs✐✈❡•② ❝❛••❡❞ ♦♥ ❛•• ✐♠♠❡❞✐❛t❡ s✉❜t❡r♠s ♦❢ t❤❡ t❡r♠✳ ✻ ❙tr❛t❡❣✐❝ ❞❡❞✉❝t✐♦♥ ■♥ t❤❡ ♣r❡✈✐♦✉s s❡❝t✐♦♥✱ ✇❡ ❤❛✈❡ s❡❡♥ ❤♦✇ t❤❡ ❛❜str❛❝t str❛t❡❣② ❝♦♥❝❡♣t ✐♥st❛♥t✐❛t❡s t♦ ❝♦♥tr♦• r✉•❡✲❜❛s❡❞ ❝♦♠♣✉t❛t✐♦♥✳ ▲❡t ✉s ♥♦✇ ❡①♣•♦r❡ t❤❡ ❞❡❞✉❝t✐♦♥ s✐❞❡✳ ■♥ ♣r♦♦❢ ❛ss✐st❛♥ts s✉❝❤ ❛s ❈♦q ❬✷✶( ❛♥❞ ♣✈s ❬✹✾(✱ t❤❡ ✐♥t❡r❛❝t✐♦♥ •❛♥❣✉❛❣❡ ✭♦r ♣r♦♦❢ •❛♥❣✉❛❣❡✮ ❝♦♥t❛✐♥s t✇♦ ❦✐♥❞s ♦❢ ♣r♦♦❢ ❝♦♠♠❛♥❞s✿ t❛❝t✐❝s✱ ✇❤✐❝❤ ❝♦♥str✉❝t t❤❡ ♣r♦♦❢ tr❡❡ ❜② ❛♣♣•②✐♥❣ •♦❣✐❝❛• r✉•❡s✱ ❛♥❞ str❛t❡❣✐❡s ✇❤✐❝❤ ♣r♦✲ ✈✐❞❡ ♣r♦♦❢ s❡❛r❝❤ ❝♦♥tr♦• ✷ ✳ ■♥ t❤✐s s❡❝t✐♦♥✱ ✇❡ ♣r♦✈✐❞❡ ✐♥♥♦✈❛t✐✈❡ ❞❡✜♥✐t✐♦♥s ♦❢ t❤❡s❡ t✇♦ ❝♦♥❝❡♣ts✱ st❛rt✐♥❣ ✇✐t❤ t❛❝t✐❝s✳ ✻✳✶ Pr♦♦❢ r❡✇r✐t✐♥❣ ❲❡ ❞❡s❝r✐❜❡ t❤❡ ♣r♦♦❢ ❝♦♥str✉❝t✐♦♥ ♠❡❝❤❛♥✐s♠ ✉s✐♥❣ t❤❡ ❛❜str❛❝t r❡❞✉❝✲ t✐♦♥ s②st❡♠ ❢r❛♠❡✇♦r❦✳ ❖✉r ♣✉r♣♦s❡ ✐♥ t❤✐s s❡❝t✐♦♥ ✐s ♥♦t t♦ ❢♦r♠❛•✐③❡ ❛♥② ♣❛rt✐❝✉•❛r ✐♥st❛♥❝❡ ♦❢ ❛ ❞❡❞✉❝t✐♦♥ s②st❡♠✱ s✉❝❤ ❛s ❝•❛ss✐❝❛• ♥❛t✉r❛• ❞❡❞✉❝✲ t✐♦♥ ❬✺✷( ♦r ✐♥t✉✐t✐♦♥✐st✐❝ s❡q✉❡♥t ❝❛•❝✉•✉s ❬✷✹(✿ ♦✉r ♠♦❞❡• ✐s s❡t✲t❤❡♦r❡t✐❝✳ |♦✉❣❤•②✱ s❡q✉❡♥ts✴t②♣✐♥❣ •✉❞❣❡♠❡♥ts ❛r❡ ❝♦♠♣♦s❡❞ ♦❢ ❛ ✜♥✐t❡ s❡t ♦❢ •❛❜❡••❡❞ ❤②♣♦t❤❡s❡s✱ ❛ ✜♥✐t❡ s❡t ♦❢ •❛❜❡••❡❞ ❝♦♥❝•✉s✐♦♥s✱ ❛♥❞ ❛ ♣r♦♦❢ t❡r♠✳ ❉❊❋■◆■❚■❖◆ ✶✾ ✭▲❛❜❡••❡❞ ♣r♦♣♦s✐t✐♦♥✮✳ •✐✈❡♥ ❛ ♣r♦♦❢ t❡r♠ •❛♥❣✉❛❣❡ T ❛♥❞ ❛ •♦❣✐❝❛• •❛♥❣✉❛❣❡ L✱ ❛ •❛❜❡••❡❞ ♣r♦♣♦s✐t✐♦♥ ✐s ❛ ♣❛✐r ❝♦♥s✐st✐♥❣ ♦❢ ❛ ♣r♦♦❢ t❡r♠ π ∈ T ❛♥❞ ❛ •♦❣✐❝❛• ♣r♦♣♦s✐t✐♦♥ A ∈ L✱ ♥♦t❡❞ π : A✳ ❉❊❋■◆■❚■❖◆ ✷✵ ✭❙❡q✉❡♥t✮✳ •✐✈❡♥ ❛ ♣r♦♦❢ t❡r♠ •❛♥❣✉❛❣❡ T ❛♥❞ ❛ •♦❣✐❝❛• •❛♥❣✉❛❣❡ L✱ ❛ s❡q✉❡♥t ✐s ❛ tr✐♣•❡ s = (π, Γ, ∆)✱ ✇❤❡r❡ π ✐s ❛ ♣r♦♦❢ t❡r♠ ♦❢ T ✱ ❛♥❞ ✇❤❡r❡ Γ ❛♥❞ ∆ ✭r❡s♣❡❝t✐✈❡•② t❤❡ ❛♥t❡❝❡❞❡♥t ❛♥❞ t❤❡ ❝♦♥s❡q✉❡♥t✮ ❛r❡ ✜♥✐t❡ s❡ts ♦❢ •❛❜❡••❡❞ ♣r♦♣♦s✐t✐♦♥s ♦❢ L✳ ■♥ t❤❡ ❢♦••♦✇✐♥❣✱ t❤✐s tr✐♣•❡ ✇✐•• ❜❡ ❞❡♥♦t❡❞✿ π ∴ (Γ ⊢ ∆)✱ ♦r ✐♥ s❤♦rt π ∴ s✳ ❚❤❡ ✭✐♥✜♥✐t❡✮ s❡t ♦❢ s❡q✉❡♥ts ✇✐•• ❜❡ ❞❡♥♦t❡❞ S(T , L)✳ ❚❤✐s r❡♣r❡s❡♥t❛t✐♦♥ ♦❢ s❡q✉❡♥ts ❞✐✛❡rs ❢r♦♠ t❤❡ ✉s✉❛• ❞❡✜♥✐t✐♦♥✱ ❣✐✈❡♥ ✐♥ ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥✱ ✇❤❡r❡ ❛•• ♣r♦♦❢ t❡r♠s ❛r❡ ❛tt❛❝❤❡❞ t♦ ❛ ♣r♦♣♦s✐t✐♦♥ ✐♥ t❤❡ ❛♥t❡❝❡❞❡♥t ♦r ✐♥ t❤❡ ❝♦♥s❡q✉❡♥t✱ ❛♥❞ ❛ s❡q✉❡♥t ✐s •✉st t❤❡ ♣❛✐r Γ ⊢ ∆✳ ✷ ❱❛r✐♦✉s ♦t❤❡r t❡r♠✐♥♦•♦❣✐❡s ❡①✐st ✐♥ t❤✐s ✜❡•❞✿ ❢♦r ✐♥st❛♥❝❡✱ ♣✈s t❛❝t✐❝s ❛r❡ ❝❛••❡❞ ♣r♦♦❢ r✉•❡s✱ ✇❤✐•❡ ❈♦q str❛t❡❣✐❡s ❛r❡ ♥❛♠❡s t❛❝t✐❝❛•s✳ ❲❡ ✉s❡ t❤❡ ✇♦r❞s ✏t❛❝t✐❝✑ ❛♥❞ ✏str❛t❡❣②✑ ❜❡❝❛✉s❡ t❤❡② ❛♣♣r♦♣r✐❛t❡•② ❝♦♥✈❡② ❛ ♥♦t✐♦♥ ♦❢ •♦❝❛•✐t②✳ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✶✺ ❚❤❡ ✉s✉❛• r❡♣r❡s❡♥t❛t✐♦♥ ❝❛♥ ❜❡ ❡♥❝♦❞❡❞ ✐♥ ♦✉r ❢♦r♠❛•✐s♠ ✉s✐♥❣ ❛ r❡s❡r✈❡❞ ❢♦r♠✉•❛ •❛❜❡• ❵ * ✬✱ ❛s ✐••✉str❛t❡❞ ❜② t❤❡ ❢♦••♦✇✐♥❣ ❡①❛♠♣•❡✿ ❊❳❆▼P▲❊ ✷✶✳ ▲❡t ✉s t❛❦❡ Λ✱ t❤❡ s❡t ♦❢ s✐♠♣•② t②♣❡❞ •❛♠❜❞❛✲t❡r♠s✱ ❢♦r T ✱ ❛♥❞ ❢♦•✱ t❤❡ s❡t ♦❢ ❛•• ✜rst✲♦r❞❡r ♣r♦♣♦s✐t✐♦♥s✱ ❢♦r L✳ ❚❤❡ s❡q✉❡♥t st❛t✐♥❣ t❤❛t ✉♥❞❡r t❤❡ ❛ss✉♠♣t✐♦♥ ✭t : A✮✱ ♦♥❡ ♦❢ t❤❡ st❛t❡♠❡♥ts (λx.t : B ⇒ A) ♦r (u : C) ✐s ♣r♦✈❛❜•❡✱ ✐s ❞❡♥♦t❡❞ ✐♥ ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥✿ t : A ⊢ λx.t : B ⇒ A, u : C ❆ss✉♠❡ ❛ ♣r♦♦❢ ♦❢ t❤✐s s❡q✉❡♥t ❜❡❣✐♥s ✇✐t❤ t❤❡ ❞❡❝♦♥str✉❝t✐♦♥ ♦❢ t❤❡ λ✲ ♣r♦♦❢ t❡r♠ λx.t✱ ✉s✐♥❣ t❤❡ ✏ ⇒✲✐♥tr♦✑ ❞❡❞✉❝t✐♦♥ r✉•❡✳ ❙✐♥❝❡ ✐t ✐s t❤❡ ❝❡♥tr❛• ❡•❡♠❡♥t ♦❢ t❤❡ ♥❡①t ❞❡❞✉❝t✐♦♥ st❡♣✱ t❤✐s ♣r♦♦❢ t❡r♠ ❤❛s ❛ ♣❛rt✐❝✉•❛r st❛t✉s✱ ❛♥❞ ❝❛♥ ❜❡ q✉❛•✐✜❡❞ ❛s ♣✐✈♦t❛•✳ ■♥ ♦r❞❡r t♦ ❡①♣r❡ss t❤❡ ❛❢♦r❡♠❡♥t✐♦♥❡❞ s❡q✉❡♥t ✇✐t❤✐♥ t❤❡ ❢r❛♠❡✇♦r❦ s❡t ❜② ❉❡✜♥✐t✐♦♥ ✷✵✱ t❤❡ ♣✐✈♦t❛• ♣r♦♦❢ t❡r♠ ✐s s❡♣❛r❛t❡❞ ❢r♦♠ ✐ts ♣r♦♣♦s✐t✐♦♥✱ ❛♥❞ t❤❡ ❵ * ✬ ♣•❛❝❡❤♦•❞❡r ♣✉t ✐♥ ✐ts ♣•❛❝❡ t♦ •❛❜❡• t❤❡ ♣r♦♣♦s✐t✐♦♥✳ ❍❡♥❝❡ t❤❡ s❡q✉❡♥t ✐s ✇r✐tt❡♥✿ λx.t ∴ (t : A ⊢ * : B ⇒ A, u : C) ❙✐♥❝❡ ❛ ♣✐✈♦t❛• ♣r♦♦❢ t❡r♠ ❝❛♥ ❛•✇❛②s ❜❡ ♣✐♥♣♦✐♥t❡❞✱ s✉❝❤ ❛ tr❛♥s❢♦r♠❛t✐♦♥ ❝❛♥ ❜❡ ♠❛❞❡ ♦♥ ❛♥② s❡q✉❡♥t ♦❢ ❛ ♣r♦♦❢ ✐♥ ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥✳ ❖♥ t❤❡ ♦t❤❡r ❤❛♥❞✱ s❡♣❛r❛t✐♥❣ t❤❡ ♣r♦♦❢ t❡r♠ ❢r♦♠ t❤❡ ❛♥t❡❝❡❞❡♥t ❛♥❞ ❝♦♥s❡q✉❡♥t ❛••♦✇s ✉s t♦ ❝❛♣t✉r❡ ♠♦r❡ ✐♥✈♦•✈❡❞ •♦❣✐❝❛• s❡tt✐♥❣s✱ ✇❤❡r❡ t❤❡ ♣✐✈♦t❛• ♣r♦♦❢ t❡r♠s ♠✐❣❤t ❛♣♣❡❛r✱ ♥♦t ♦♥•② ❛t t❤❡ •❡✈❡• ♦❢ ❢♦r♠✉•❛s✱ ❜✉t ❛•s♦ ❛t t❤❡ •❡✈❡• ♦❢ s❡q✉❡♥ts✳ ❋♦r ✐♥st❛♥❝❡✱ ✐♥ t❤❡ ❝❛s❡ ♦❢ s❡q✉❡♥t ❝❛•❝✉•✉s à •❛ ❈✉r✐❡♥✲❍❡r❜❡•✐♥ ❬✶✼(✱ t❤❡ s❡q✉❡♥ts Γ ⊢ λx.v : A ⇒ B; ∆ ❛♥❞ v|e : (Γ ⊢ ∆)✱ ✇❤❡r❡ λx.v ❛♥❞ v|e ❛r❡ ♣✐✈♦t❛• λµμ✲♣r♦♦❢ t❡r♠s✱ ❛r❡ ✇❡••✲❢♦r♠❡❞✳ ■♥ ♦✉r ❢♦r♠❛•✐s♠✱ ✇❤✐•❡ t❤❡ ✜rst s❡q✉❡♥t ✐s ❡①♣r❡ss❡❞ ✉s✐♥❣ t❤❡ ❛❢♦r❡♠❡♥t✐♦♥❡❞ ❵ * ✬ •❛❜❡• ✉s✐♥❣ t❤❡ s❛♠❡ ♣r♦❝❡ss ❛s ✐♥ ❊①❛♠♣•❡ ✷✶✱ t❤❡ s❡❝♦♥❞ s❡q✉❡♥t ✐s tr✐✈✐❛••② r❡♣r❡s❡♥t❡❞ ❜② t❤❡ ✐s♦♠♦r♣❤✐❝ tr✐♣•❡ v|e ∴ (Γ ⊢ ∆)✱ ✐♥ ✇❤✐❝❤ ♥♦ ❵ * ✬ •❛❜❡• ❛♣♣❡❛r✳ ❚❤❡ s❛♠❡ ❤♦•❞s ❢♦r ❯r❜❛♥✬s s❡q✉❡♥t ❝❛•❝✉•✉s ❬✺✺(✱ ✇❤✐❝❤ ♣•❛❝❡s ❛•• ♣r♦♦❢ t❡r♠s ♦♥ t❤❡ s❛♠❡ •❡✈❡• ❛s t❤❡ ❛♥t❡❝❡❞❡♥ts ❛♥❞ ❝♦♥s❡q✉❡♥ts✳ ❋✐♥❛••② ✇❡ ♥❡❡❞ t♦ ❛❞❞ ❛ ♥♦t✐♦♥ ♦❢ •✐st ♦❢ s❡q✉❡♥ts✿ t❤❡r❡❢♦r❡ ✇❡ ✐♥tr♦❞✉❝❡ t❤❡ ✉s✉❛• •✐st ❝♦♥str✉❝t♦rs ❝♦♥s ❛♥❞ ♥✐•✱ ♥♦t❡❞ ❵;✬ ❛♥❞ ❵∅✬✳ ❋♦r t②♣❡s❡tt✐♥❣ ♣✉r♣♦s❡s ❛♥❞ ✇❤❡♥ ✉♥❛♠❜✐❣✉♦✉s✱ ✇❡ ❛❜❜r❡✈✐❛t❡ t❤❡ •✐st φ; ∅ t♦ φ✱ ❛♥❞ ✇❡ ♦♠✐t ❛•• •✐st ❝♦♥str✉❝t♦rs ❢♦r ✉♥❛r② •✐sts✳ ❋✐♥❛••②✱ t❤❡ ♥♦t✐♦♥ ♦❢ s✉❜st✐t✉t✐♦♥ ❝❛rr✐❡❞ ❜② t❡r♠s ❛♥❞ ♣r♦♣♦s✐t✐♦♥s ✐s ❡❛s✐•② ❡①t❡♥❞❡❞ t❤r♦✉❣❤ s✐♠♣•❡ s✉❜t❡r♠ ♣r♦♣❛❣❛t✐♦♥ t♦ r❛♥❣❡ ♦✈❡r s❡q✉❡♥ts ❛♥❞ •✐sts ♦❢ s❡q✉❡♥ts✳ ❚❤❡ s❡t ♦❢ •✐sts ♦❢ s❡q✉❡♥ts ✐s ❞❡♥♦t❡❞ LS(T , L)✳ ❆ ❞❡❞✉❝t✐♦♥ s②st❡♠ ❝❛♥ ❜❡ s❡❡♥ ❛s ❛ r❡✇r✐t❡ s②st❡♠ ♦♣❡r❛t✐♥❣ ♦♥ t②♣❡❞ ♣r♦♦❢ t❡r♠s✱ ✐✳❡✳✱ s❡q✉❡♥ts✳ ❚❤❡ ❢♦••♦✇✐♥❣ ❞❡✜♥✐t✐♦♥s •❛② t❤❡ ❣r♦✉♥❞✇♦r❦ ❛♥❞ •❡❛❞ t♦ t❤❡ ❡①♣r❡ss✐♦♥ ♦❢ ❞❡❞✉❝t✐♦♥ s②st❡♠s ❛s ✐♥st❛♥❝❡s ♦❢ t❤❡ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ ❢r❛♠❡✇♦r❦✳ ❉❊❋■◆■❚■❖◆ ✷✷ ✭❉❡❞✉❝t✐♦♥ r✉•❡✮✳ ❆ r❡✇r✐t❡ r✉•❡✱ ❛•s♦ ❝❛••❡❞ ❞❡❞✉❝t✐♦♥ r✉•❡✱ ❝♦♥♥❡❝ts ❛ s✐♥❣•❡ s❡q✉❡♥t t♦ ❛ •✐st ♦❢ s❡q✉❡♥ts✿ l ∴ (Γ l ⊢ ∆ l ) → r 1 ∴ (Γ r1 ⊢ ∆ r1 ); . . . ; r n ∴ (Γ rn ⊢ ∆ rn ) ■♥ ♦r❞❡r t♦ ❝❛♣t✉r❡ t❤❡ ❡①♣r❡ss✐✈✐t② ♦❢ •♦❣✐❝❛• r✉•❡s✱ r❡✇r✐t❡ r✉•❡s ✐♥ t❤✐s ❝♦♥t❡①t ♠❛② ❤❛✈❡ ❛ ✈❛r✐❛❜•❡ ❛s •❡❢t✲❤❛♥❞ s✐❞❡ ❛♥❞ ♠❛② ✐♥tr♦❞✉❝❡ ✐♥ t❤❡ r✐❣❤t✲ ❤❛♥❞ s✐❞❡ s♦♠❡ ✈❛r✐❛❜•❡s t❤❛t ❞♦ ♥♦t ♦❝❝✉r ✐♥ t❤❡ •❡❢t✲❤❛♥❞ s✐❞❡✳ ■♥❞❡❡❞✱ r❡•❛①✐♥❣ t❤❡s❡ s②♥t❛❝t✐❝ r❡str✐❝t✐♦♥s ♠❛❦❡s ❡✈❡♥ ♠♦r❡ ❝r✉❝✐❛• t❤❡ ♥❡❡❞ ♦❢ ❝♦♥tr♦••✐♥❣ r✉•❡ ❛♣♣•✐❝❛t✐♦♥ t❤❛♥❦s t♦ str❛t❡❣✐❡s✳ ❉❊❋■◆■❚■❖◆ ✷✸ ✭❖♥❡ st❡♣ ❞❡❞✉❝t✐♦♥✮✳ ❲❡ s❛② t❤❛t t❤❡ s❡q✉❡♥t •✐st φ = π 1 ∴ s 1 ; . . . ; π m ∴ s m r❡❞✉❝❡s ✐♥ ♦♥❡ st❡♣ t♦ t❤❡ s❡q✉❡♥t •✐st φ ′ ❜② t❤❡ ❞❡❞✉❝t✐♦♥ r✉•❡ l ∴ s l → r 1 ∴ s 1 ; . . . ; r n ∴ s n ✐❢ ❛♥❞ ♦♥•② ✐❢ t❤❡r❡ ❡①✐sts ❛ s✉❜st✐t✉t✐♦♥ σ s✉❝❤ t❤❛t π i ∴ s i = σ(l ∴ s l ) ❛♥❞ φ ′ = π 1 ∴ s 1 ; . . . ; π i-1 ∴ s i-1 ; σ(r 1 ∴ s 1 ; . . . ; r n ∴ s n ); π i+1 ∴ s i+1 ; . . . ; π m ∴ s m ❲❤❡♥ ❛♣♣r♦♣r✐❛t❡✱ t❤❡ ♠❛t❝❤✐♥❣ st❡♣ ✉s❡❞ ✐♥ t❤❡ ♣r❡✈✐♦✉s ❞❡✜♥✐t✐♦♥ ❝❛♥ ❜❡ ❛♣♣•✐❡❞ ♠♦❞✉•♦ ❛♥ ❡q✉❛t✐♦♥❛• t❤❡♦r②✱ •✐❦❡ ✐♥ t❤❡ ❢♦••♦✇✐♥❣ ❡①❛♠♣•❡✳ ❊❳❆▼P▲❊ ✷✹✳ ❋✐rst✲♦r❞❡r ♠✐♥✐♠❛• ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥ ✐s ♣❡r❤❛♣s t❤❡ ♠♦st ✇❡••✲❦♥♦✇♥ •♦❣✐❝❛• ❢r❛♠❡✇♦r❦ t♦ s✉♣♣♦rt t❤❡ ♣r♦♦❢✲❛s✲t❡r♠s ♠♦r♣❤✐s♠✳ ■t ❝♦♥s✐❞❡rs ✜rst✲♦r❞❡r ♣r♦♣♦s✐t✐♦♥s ❛s t②♣❡s ❢♦r •❛♠❜❞❛✲t❡r♠s✱ ❛♥❞ ❤❛s t②♣✐♥❣ •✉❞❣❡♠❡♥ts ♦❢ t❤❡ ❢♦r♠ Γ ⊢ t : A✳ ■♥ ♦✉r ❢♦r♠❛•✐s♠✱ ✇❡ ❤❛✈❡ T = Λ✱ L = ❢♦• ❛♥❞ s❡q✉❡♥ts ♦❢ t❤❡ ❢♦r♠ t ∴ (Γ ⊢ * : A)✳ ❚❤❡ ❞❡❞✉❝t✐♦♥ r✉•❡s ❢♦r ♠✐♥✐♠❛• ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥ ❝❛♥ ❜❡ ❡①♣r❡ss❡❞ ❛s t❤❡ ❢♦••♦✇✐♥❣ r❡✇r✐t❡ r✉•❡s✱ ✇❤❡r❡ Γ ✐s ❛ ✈❛r✐❛❜•❡ r❡♣r❡s❡♥t✐♥❣ ❛ ♠✉•t✐s❡t ♦❢ ♣r♦♣♦s✐t✐♦♥s ✭✐✳❡✳✱ t❤❡ s❡♣❛r❛t♦r ✏✱✑ ✐s ❛ss♦❝✐❛t✐✈❡ ❛♥❞ ❝♦♠♠✉t❛t✐✈❡✮✱ t, u ❛r❡ ♣r♦♦❢ t❡r♠ ✈❛r✐❛❜•❡s✱ A, B ❛r❡ ♣r♦♣♦s✐t✐♦♥ ✈❛r✐❛❜•❡s✳ I ∴ (Γ ⊢ * : ⊤) → ∅ ✭D 1 ✮ t ∴ (Γ, t : A ⊢ * : A) → ∅ ✭D 2 ✮ λx.t ∴ (Γ ⊢ * : A ⇒ B) → t ∴ (Γ, x : A ⊢ * : B) ✭D 3 ✮ tu ∴ (Γ ⊢ * : B) → t ∴ (Γ ⊢ * : A ⇒ B); u ∴ (Γ ⊢ * : A) ✭D 4 ✮ λx.t ∴ (Γ ⊢ * : ∀xB) → t ∴ (Γ ⊢ * : B) ✭D 5 ✮ tu ∴ (Γ ⊢ * : B[u] ω ) → t ∴ (Γ ⊢ * : ∀xB[x] ω ) ✭D 6 ✮ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✶✼ ✇❤❡r❡ I ✐s ❛ ♣r♦♦❢ t❡r♠ ❝♦♥st❛♥t✳ ◆♦t✐❝❡ t❤❡ ✉s❡ ♦❢ ❛ ❢r❡❡ ✈❛r✐❛❜•❡ A ✭r❡s♣✳ x✮ ✐♥ t❤❡ r✐❣❤t ❤❛♥❞✲s✐❞❡ ♦❢ r✉•❡ ✭D 4 ✮ ✭r❡s♣✳ ✭D 6 ✮✮✳ ❇❛s❡❞ ♦♥ t❤✐s s❡t ♦❢ r❡✇r✐t❡ r✉•❡s✱ ❛ s❡r✐❡s ♦❢ ❢♦✉r r❡❞✉❝t✐♦♥ st❡♣s ❝♦✉•❞ ❜❡✿ λx.λy. (yx) ∴ (⊢ * : A ⇒ (A ⇒ B) ⇒ B) → ✭D3✮ λy. (yx) ∴ (x : A ⊢ * : (A ⇒ B) ⇒ B) → ✭D3✮ (yx) ∴ (x : A, y : A ⇒ B ⊢ * : B) → ✭D4✮ y ∴ (x : A, y : A ⇒ B ⊢ * : A ⇒ B); x ∴ (x : A, y : A ⇒ B ⊢ * : A) → ✭D2✮ ∅; ∅ ◆♦t❡ t❤❛t ✐♥ t❤❡ ♣r❡✈✐♦✉s ❡①❛♠♣•❡✱ t❤❡ r✉•❡ ✭D 2 ✮ ❝❛♥ ❜❡ ❛♣♣•✐❡❞ ❜❡❝❛✉s❡ ✇❡ ❛ss✉♠❡ t❤❡ s②♠❜♦• ✏✱✑ t♦ ❜❡ ❛ss♦❝✐❛t✐✈❡ ❛♥❞ ❝♦♠♠✉t❛t✐✈❡✳ ❆♥♦t❤❡r ♣♦ss✐❜✐•✐t② ❝♦✉•❞ ❜❡ t♦ ❛❞❞ ❛ ❝♦♠♠✉t❛t✐♦♥ r✉•❡✱ ✇✐t❤ t❤❡ r✐s❦ t♦ ✐♥❤❡r✐t ♦❢ t❤❡ ❡①♣•✐❝✐t tr❡❛t♠❡♥t ♦❢ ❝♦♠♠✉t❛t✐✈✐t② ❛t t❤❡ ♣r♦♦❢ ❞❡s✐❣♥ •❡✈❡•✳ ❉❊❋■◆■❚■❖◆ ✷✺ ✭❉❡❞✉❝t✐♦♥ s②st❡♠✮✳ •✐✈❡♥ ❛ •♦❣✐❝❛• •❛♥❣✉❛❣❡ L ❛♥❞ ❛ t❡r♠ ❛•❣❡❜r❛ T ✱ ❛ ❞❡❞✉❝t✐♦♥ s②st❡♠ ✐s ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ R = (O R , S R ) ✇❤❡r❡✿ • O R ❝♦♥t❛✐♥s ❡•❡♠❡♥ts ♦❢ LS(T , L)✱ ❛♥❞ • S R = {φ → φ ′ | φ -→ φ l →φr ω φ ′ } ✇❤❡r❡ ω ✐s ❛ ♣♦s✐t✐♦♥ ✐♥ φ ✭✐✳❡✳✱ ♦♥❡ ♦❢ ✐ts s❡q✉❡♥ts✮ ❛♥❞ φ l → φ r ✐s ❛ ❞❡❞✉❝t✐♦♥ r✉•❡✳ ❆s ❢♦r t❡r♠ r❡✇r✐t✐♥❣✱ ✇❡ ✇✐•• ❤❡r❡❛❢t❡r ✉s❡ ❛•• t❤❡ ❞❡✜♥✐t✐♦♥s ❣✐✈❡♥ ✐♥ t❤❡ ❛❜str❛❝t ❝❛s❡ ❢♦r ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠s✳ ❋♦r ❛ ❣✐✈❡♥ ❞❡❞✉❝t✐♦♥ s②st❡♠ DS✱ ❛ ❝♦♠♣•❡t❡❞ ♣r♦♦❢ ♦❢ ❛ s❡q✉❡♥t φ ✐s ❛ ❞❡r✐✈❛t✐♦♥ ✐ss✉❡❞ ❢r♦♠ φ ❛♥❞ r❡❛❝❤✐♥❣ t❤❡ •✐st ∅; . . . ; ∅ ✉s✐♥❣ t❤❡ r✉•❡s ✐♥ DS✳ ■t ✐s ✐♠♣♦rt❛♥t t♦ ♥♦t✐❝❡ t❤❛t t❤❡ ♥♦t✐♦♥ ♦❢ ❞❡r✐✈❛t✐♦♥ ❝♦♥s✐❞❡r❡❞ ❤❡r❡ ❝♦♥❝❡r♥s ❛ ❢✉•• ♣r♦♦❢ tr❡❡ ❛♥❞ ♥♦t ♦♥•② ♦♥❡ ♦❢ ✐ts ❜r❛♥❝❤❡s✳ ❚❤✐s ✐s ❞✉❡ t♦ t❤❡ ❢❛❝t t❤❛t ✇❡ ✇❛♥t t♦ ❞❡✜♥❡ str❛t❡❣✐❡s ❛❜•❡ t♦ ❝♦♥s✐st❡♥t•② ❞❡✈❡•♦♣ ❝♦♠♣•❡t❡ ♣r♦♦❢ tr❡❡s ❛♥❞ ♥♦t ♦♥•② ♣❛rt ♦❢ t❤❡♠✳ ❚❤❡r❡❢♦r❡✱ t❤❡ ♥♦t✐♦♥s ♦❢ ❞❡❞✉❝t✐♦♥ s②st❡♠s ❛♥❞ ♦❢ str❛t❡❣✐❡s ❛r❡ ❞❡✜♥❡❞ ❛❝❝♦r❞✐♥❣•② ♦♥ •✐sts ♦❢ s❡q✉❡♥ts r❡♣r❡s❡♥t✐♥❣ ♣r♦♦❢ tr❡❡s✳ ❋♦••♦✇✐♥❣ t❤❡s❡ ❞❡✜♥✐t✐♦♥s✱ ❝♦♠♣•❡t❡❞ ♣r♦♦❢s ❛r❡ ❝❛r❛❝t❡r✐③❡❞ ❛s r❡❞✉❝✲ t✐♦♥ s❡q✉❡♥❝❡s✱ ♦r ❡q✉✐✈❛•❡♥t•② ❛s ♣❛t❤s ✐♥t♦ t❤❡ ❆|❙ ❢♦r♠❡❞ ❜② ❛ ❞❡❞✉❝t✐♦♥ s②st❡♠✳ ❍♦✇❡✈❡r✱ t❤✐s •❡❛✈❡s t❤❡ q✉❡st✐♦♥ ♦❢ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ ❛ ♣r♦♦❢✱ ✐✳❡✳✱ ♦❢ ❛ ♣r♦♦❢ t❡r♠✱ ✉♥❛♥s✇❡r❡❞✳ (❡t t❤✐s ✐s ❛ ❢✉♥❞❛♠❡♥t❛• ♠❡❝❤❛♥✐s♠ ✐♥ t❤❡ ❞❡s✐❣♥ ♦❢ ♣r♦♦❢ ❛ss✐st❛♥ts✳ ■♥ ♦r❞❡r t♦ ❛❞❞r❡ss t❤✐s q✉❡st✐♦♥✱ ✈❛r✐♦✉s ❛✉t❤♦rs ❬✹✸✱ ✹✼✱ ✸✵( ❤❛✈❡ s❤♦✇♥ t❤❛t t❤❡ s②♥t❛① ♦❢ ♣r♦♦❢ t❡r♠s ❛♥❞ s❡q✉❡♥ts ❝❛♥ ❜❡ ❡①t❡♥❞❡❞ ✇✐t❤ ♣r♦♦❢ ♠❡t❛✈❛r✐❛❜•❡s✱ t❤❛t r❡♣r❡s❡♥t t❤❡ st✐•• ✉♥❦♥♦✇♥ ♣❛rts ♦❢ ❛ ♣r♦♦❢✳ ❉❊❋■◆■❚■❖◆ ✷✻ ✭Pr♦♦❢ ♠❡t❛✈❛r✐❛❜•❡s✮✳ ❈♦♥s✐❞❡r t❤❡ s②♥t❛① ♦❢ ♣r♦♦❢ t❡r♠s ❡①t❡♥❞❡❞ ✇✐t❤ ❛ s♣❡❝✐❛• s❡t ♦❢ ✈❛r✐❛❜•❡s M✱ ❝❛••❡❞ ♠❡t❛✈❛r✐❛❜•❡s✱ ♥♦t❡❞ X, Y, Z✳ ✳ ✳ ✳ ❲❡ ♥♦t❡ T M t❤❡ ❛•❣❡❜r❛ ♦❢ ♣r♦♦❢ t❡r♠s ✇✐t❤ ♠❡t❛✈❛r✐❛❜•❡s✱ ❛♥❞ meta(π) t❤❡ s❡t ♦❢ ♠❡t❛✈❛r✐❛❜•❡s ❛♣♣❡❛r✐♥❣ ✐♥ π✳ ❲❡ ❝❛•• ♦♣❡♥ s❡q✉❡♥t ❛ tr✐♣•❡ π ∴ (Γ ⊢ ∆) ✇❤❡r❡ π ❝♦♥t❛✐♥s ❛t •❡❛st ♦♥❡ ♠❡t❛✈❛r✐❛❜•❡✳ ❆s s❤♦✇♥ ✐♥ ❬✹✼(✱ t❤❡ ✉s❡ ♦❢ ♠❡t❛✈❛r✐❛❜•❡s ✐♥ •♦❣✐❝❛• s❡tt✐♥❣s ❢❡❛t✉r✐♥❣ ❞❡♣❡♥❞❡♥t t②♣❡s ♦r ♣♦•②♠♦r♣❤✐s♠ r❡q✉✐r❡s t❤❡ ❛❞❞✐t✐♦♥ ♦❢ ❝♦♥str❛✐♥ts t♦ t❤❡ r❡♣r❡s❡♥t❛t✐♦♥ ♦❢ s❡q✉❡♥ts✳ ❙✐♥❝❡ t❤✐s ❡①t❡♥s✐♦♥ ✐s ♠♦r❡ ❡•❛❜♦r❛t❡❞✱ ✐♥t❡r❡st✐♥❣ ❜✉t •❛r❣❡•② ♦rt❤♦❣♦♥❛• t♦ ♦✉r ❝✉rr❡♥t ♣✉r♣♦s❡✱ ✐t ✇✐•• ♥♦t ❜❡ ❢✉rt❤❡r ❞❡t❛✐•❡❞ ✐♥ t❤✐s ♣❛♣❡r✳ ❉❊❋■◆■❚■❖◆ ✷✼ ✭Pr♦♦❢ ❣r❛❢t✐♥❣ r✉•❡✮✳ ❆ ♣r♦♦❢ ❣r❛❢t✐♥❣ r✉•❡ ✐s ❛♥ ♦r❞❡r❡❞ ♣❛✐r ♦❢ s❡q✉❡♥ts✱ ❞❡♥♦t❡❞ L ∴ s → r ∴ s✱ ✇❤❡r❡ L ✐s ❛ ♣r♦♦❢ ♠❡t❛✈❛r✐❛❜•❡ ❛♥❞ r ♠❛② ♦r ♠❛② ♥♦t ❝♦♥t❛✐♥ ♠❡t❛✈❛r✐❛❜•❡s✳ ❆ ♣r♦♦❢ ❝♦♥str✉❝t✐♦♥ st❡♣ ❝❛♥ t❤❡♥ ❜❡ s✐♠♣•② ❞❡✜♥❡❞ ❛s t❤❡ ❛♣♣•✐❝❛t✐♦♥ ♦❢ ❛ ♣r♦♦❢ ❣r❛❢t✐♥❣ r✉•❡ t♦ ❛ •✐st ♦❢ s❡q✉❡♥ts✱ s✐♠✐•❛r•② t♦ ❉❡✜♥✐t✐♦♥ ✷✸✳ ❚❤❡ s❡q✉❡♥t ❢❡❛t✉r✐♥❣ t❤❡ ♥❡✇•② ✐♥tr♦❞✉❝❡❞ ♣r♦♦❢ t❡r♠ ✐s t❤❡♥ r❡❞✉❝❡❞ ✉s✐♥❣ ❞❡❞✉❝t✐♦♥ r✉•❡s✱ ✉♥t✐• t❤❡ ♣r♦♦❢ ❡♥❞s ♦r ❛ ♥❡✇ ❣r❛❢t✐♥❣ st❡♣ ✐s ♥❡❝❡ss❛r②✳ ❊❳❆▼P▲❊ ✷✽✳ |❡❝❛•• t❤❡ ♠✐♥✐♠❛• ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥ ❢♦r♠❛•✐s♠ ♣r❡s❡♥t❡❞ ✐♥ ❊①❛♠♣•❡ ✷✹✳ ❆ss✉♠❡ t❤❡ ❢♦••♦✇✐♥❣ r✉•❡s ❢♦r ♠❡t❛✈❛r✐❛❜•❡ ✐♥st❛♥t✐❛t✐♦♥✿ X ∴ (Γ ⊢ * : ⊤) → I ∴ (Γ ⊢ * : ⊤) ✭C 1 ✮ X ∴ (Γ, x : A ⊢ * : A) → x ∴ (Γ, x : A ⊢ A) ✭C 2 ✮ X ∴ (Γ ⊢ * : A ⇒ B) → λx A .Y ∴ (Γ ⊢ * : A ⇒ B) ✭C 3 ✮ X ∴ (Γ ⊢ * : A) → (YZ) ∴ (Γ ⊢ * : A) ✭C 4 ✮ X ∴ (Γ ⊢ * : ∀xB) → λx.t ∴ (Γ ⊢ * : ∀xB) ✭C 5 ✮ X ∴ (Γ ⊢ * : B[u] ω ) → tu ∴ (Γ ⊢ * : B[u] ω ) ✭C 6 ✮ ❲❤✐•❡ t❤❡ ♣r♦♦❢ ❣r❛❢t✐♥❣ r✉•❡s ❝❛♥ ❜❡ ❛r❜✐tr❛r✐•② ❝❤♦s❡♥✱ t❤❡s❡ s✐① r✉•❡s ❡❛❝❤ ❞❡s❝r✐❜❡ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ ❛ λ✲♣r♦♦❢ t❡r♠ ❤❡❛❞ s②♠❜♦•✳ ❋✉rt❤❡r♠♦r❡✱ ✐t ✐s ❡❛s② t♦ ✈❡r✐❢② t❤❛t t❤❡② ❜✉✐•❞ ♣r♦♦❢s t❡r♠s t❤❛t ❝❛♥ ❜❡ t②♣❡❝❤❡❝❦❡❞ ✉s✐♥❣ t❤❡ ❞❡❞✉❝t✐♦♥ r✉•❡s ❢♦r ♥❛t✉r❛• ❞❡❞✉❝t✐♦♥✳ ❇❛s❡❞ ♦♥ t❤✐s s❡t ♦❢ r❡✇r✐t❡ r✉•❡s✱ t❤❡ ❝♦♥str✉❝t✐♦♥ ♦❢ t❤❡ ♣r♦♦❢ t❡r♠ ♦❢ ❡①❛♠♣•❡ ✷✹ ✐s ❝♦♥❞✉❝t❡❞ ❜② ❛♥ ❛•t❡r♥❛t✐♦♥ ❙tr❛t❡❣✐❝ ❈♦♠♣✉t❛t✐♦♥ ❛♥❞ ❉❡❞✉❝t✐♦♥ ✶✾ ♦❢ ❞❡❞✉❝t✐♦♥ ❛♥❞ ❣r❛❢t✐♥❣ r✉•❡s✿ X 1 ∴ (⊢ * : A ⇒ (A ⇒ B) ⇒ B) → ✭C3✮ λx A .X 2 ∴ (⊢ * : A ⇒ (A ⇒ B) ⇒ B) → ✭D3✮ X 2 ∴ (x : A ⊢ * : (A ⇒ B) ⇒ B) → ✭C3✮ λy A⇒B .X 3 ∴ (x : A ⊢ * : A ⇒ (A ⇒ B) ⇒ B) → ✭D3✮ X 3 ∴ (x : A, y : A ⇒ B ⊢ * : A ⇒ (A ⇒ B) ⇒ B) → ✭C4✮ (X 4 X 5 ) ∴ x : A, y : A ⇒ B ⊢ A ⇒ (A ⇒ B) ⇒ B → ✭D4✮ X 4 ∴ (x : A, y : A ⇒ B ⊢ * : A ⇒ B); X 5 ∴ (x : A, y : A ⇒ B ⊢ * : A) → ✭C2✮ y ∴ (x : A, y : A ⇒ B ⊢ * : A ⇒ B);

X 5 ∴

 5 (x : A, y : A ⇒ B ⊢ * : A) → ✭D2✮ ∅; X 5 ∴ (x : A, y : A ⇒ B ⊢ * : A) → ✭C2✮ ∅; x ∴ (x : A, y : A ⇒ B ⊢ * : A) → ✭D2✮ ∅; ∅ ❚❤❡ s②♥t❤❡s✐s ♦❢ t❤❡ ❣r❛❢t✐♥❣ st❡♣ ✐♥st❛♥❝❡s t❤❡♥ ②✐❡•❞s t❤❡ ✜♥❛• ♣r♦♦❢ t❡r♠✳ ❚❤❡ ❛•t❡r♥❛t❡ Ci ; D i r❡❞✉❝t✐♦♥s ❝♦rr❡s♣♦♥❞ t♦ t❤❡ •❝❢ ❞❡✜♥✐t✐♦♥ ♦❢ ❛ t❛❝t✐❝✱ ✐✳❡✳✱ ❛ ❣r❛❢t✐♥❣ st❡♣ t❤❛t ✐♥st❛♥t✐❛t❡s ❛ ♣r♦♦❢ t❡r♠ ♠❡t❛✈❛r✐❛❜•❡ ❢♦••♦✇❡❞ ❜② ❛ s❡r✐❡s ♦❢ ❞❡❞✉❝t✐♦♥ st❡♣s t❤❛t ✐♥❢❡rs ♥❡✇ ❣♦❛•s ❢r♦♠ t❤❡ r❡s✉•t✐♥❣ s❡q✉❡♥t✳ (❡t t❤✐s ❛♣♣r♦❛❝❤ ✉s✐♥❣ ♠❡t❛✈❛r✐❛❜•❡s ❛♥❞ ❣r❛❢t✐♥❣ ❝❛♥ ❜❡ s✐❣♥✐✜❝❛♥t•② ❝♦♥❞❡♥s❡❞ ❜② ✉s✐♥❣ ❛ ♠❡❝❤❛♥✐s♠ s♣❡❝✐✜❝ t♦ t❤❡ t❡r♠ r❡✇r✐t✐♥❣ ❞♦♠❛✐♥✳ ■♥❞❡❡❞✱ t❤❡ ✐♥st❛♥t✐❛t✐♦♥ ♦❢ ❛ ♠❡t❛✈❛r✐❛❜•❡ ❜② ❛ t❡r♠✱ s✉❝❤ t❤❛t t❤❡ •❛tt❡r ❜❡❝♦♠❡s r❡❞✉❝✐❜•❡ ❜② ❛ r✉•❡ ♦❢ t❤❡ ❞❡❞✉❝t✐♦♥ s②st❡♠✱ ✐s ❡①❛❝t•② ❛ ♥❛rr♦✇✐♥❣ st❡♣✱ ❛s ❞❡✜♥❡❞ ✐♥ ❉❡✜♥✐t✐♦♥ ✶✼✳ ❊❳❆▼P▲❊ ✷✾✳ ❚❤❡ ❞❡❞✉❝t✐♦♥ s②st❡♠ ♦❢ ❊①❛♠♣•❡ ✷✹ ❝❛♥ ❜❡ ✉s❡❞ t♦ ✜♥❞ ❛ ♣r♦♦❢ ♦❢ t❤❡ ♣r♦♣♦s✐t✐♦♥ A ⇒ (A ⇒ B) ⇒ B ❜② ♥❛rr♦✇✐♥❣ t❤❡ ✐♥✐t✐❛• q✉❡r② ✐♥ t❤❡ ❢♦••♦✇✐♥❣ ✇❛②✳ U ∴ (⊢ * : A ⇒ (A ⇒ B) ⇒ B) ✭D3✮ U →λx.X X ∴ (x : A ⊢ * : (A ⇒ B) ⇒ B) ✭D3✮ X →λy.Y Y ∴ (x : A; y : A ⇒ B ⊢ * : B) ✭D4✮ Y →TZ T ∴ (x : A; y : A ⇒ B ⊢ * : α ⇒ B); Z ∴ (x : A; y : A ⇒ B ⊢ * : α) ✭D2✮ α →A,T →y,Z →x ∅; ∅ ❚❤❡ ♣r♦♦❢ ❣r❛❢t✐♥❣ r✉•❡s ❝❛♥ ❜❡ r❡❝♦✈❡r❡❞ ❜② ❛♥♥♦t❛t✐♥❣ t❤❡ ✉♥✐✜❝❛t✐♦♥ ❛ss✐❣♥♠❡♥ts ✇✐t❤ t❤❡ ❛♣♣r♦♣r✐❛t❡ s❡q✉❡♥ts✿ X ∴ (Γ ⊢ * : A ⇒ B) → λx A .Y ∴ (Γ ⊢ * : A ⇒ B) Y ∴ (Γ ⊢ * : A) →(TZ) ∴ (Γ ⊢ * : A) T ∴ (Γ, x : A ⊢ * : A) → x ∴ (Γ, x : A ⊢ A) ❛♥❞ t❤❡ ❝♦♠♣✉t❡❞ ♣r♦♦❢ t❡r♠ ✐s s✐♠♣•② ♦❜t❛✐♥❡❞ ❜② ❝♦♠♣♦s✐♥❣ t❤❡ ♥❛rr♦✇✲ ✐♥❣ s✉❜st✐t✉t✐♦♥s✿ U = {α → A, T → y, Z → x}({Y →(TZ)}({X → λy.Y}(λx.X))) = λx.λy. (yx) ◆♦t✐❝❡ ✐♥ t❤❡ ♣r❡✈✐♦✉s ❡①❛♠♣•❡ t❤❡ ✉s❡ ♠❛❞❡ ♦❢ ♣r♦♦❢ t❡r♠ ✈❛r✐❛❜•❡s ✭✐✳❡✳✱ U, X, Y, Z, T✮ ❛♥❞ t❤❡ ✉s❡ ♦❢ ♦♥❡ ♣r♦♣♦s✐t✐♦♥ ✈❛r✐❛❜•❡✱ ✐✳❡✳✱ α✳ ❍❡♥❝❡✱ ✇❤✐•❡ tr❛❞✐t✐♦♥❛••② ❛ ♣r♦♦❢ ❝♦♥str✉❝t✐♦♥ s②st❡♠ ✇❛s ❞❡✜♥❡❞ ❛s ❛♥ ❛•t❡r♥❛t✐♦♥ ♦❢ ♠❡t❛✈❛r✐❛❜•❡ ❣r❛❢t✐♥❣ ❛♥❞ ❞❡❞✉❝t✐♦♥ st❡♣s✱ ✇❤❛t ❡♠❡r❣❡s ❤❡r❡ ✐s ❛ ♠♦r❡ ❝♦♥❝✐s❡ ❞❡✜♥✐t✐♦♥✱ ❜❛s❡❞ ♦♥ t❤❡ ♥❛rr♦✇✐♥❣ r❡•❛t✐♦♥ ❞❡r✐✈❡❞ ❢r♦♠ ❛ ❞❡❞✉❝t✐♦♥ s②st❡♠✳ ❉❊❋■◆■❚■❖◆ ✸✵ ✭Pr♦♦❢ ❝♦♥str✉❝t✐♦♥ s②st❡♠✮✳ •✐✈❡♥ ❛ •♦❣✐❝❛• •❛♥❣✉❛❣❡ L✱ ❛ t❡r♠ ❛•❣❡❜r❛ T ❛♥❞ ❛ ❞❡❞✉❝t✐♦♥ s②st❡♠ DS ❞❡✜♥❡❞ ❢r♦♠ ❛ s❡t D ♦❢ ♣r♦♦❢ r❡✇r✐t❡ r✉•❡s✱ ❛ ♣r♦♦❢ ❝♦♥str✉❝t✐♦♥ s②st❡♠ ✐s ❛♥ ❛❜str❛❝t r❡❞✉❝t✐♦♥ s②st❡♠ N = (O D , S D ) ✇❤❡r❡✿ • O D ❝♦♥t❛✐♥s ❡•❡♠❡♥ts ♦❢ LS(T , L)✱ ❛♥❞ • S D = {φ φ ′ | φ D ω φ ′ ❢♦r ω ❛ ♣♦s✐t✐♦♥ ✐♥ φ}✳ ❚❤✐s ❞❡✜♥✐t✐♦♥ ♣r♦✈✐❞❡s ❛♥ ❡①♣•✐❝✐t •✐♥❦ ❜❡t✇❡❡♥ t❤❡ ❞❡❞✉❝t✐♦♥ r✉•❡s✱ ✇❤✐❝❤ ❛r❡ ✉s✉❛••② ✇❡••✲❦♥♦✇♥ ❛♥❞ ❞♦❝✉♠❡♥t❡❞ ❛s ♣❛rt ♦❢ t❤❡ ✉♥❞❡r•②✐♥❣ •♦❣✐❝❛• ❢r❛♠❡✇♦r❦ ♦❢ ❛ ♣r♦♦❢ ❝♦♥str✉❝t✐♦♥ s②st❡♠✱ ❛♥❞ t❤❡ ♠❡t❛✈❛r✐❛❜•❡ ✐♥✲ st❛♥t✐❛t✐♦♥ st❡♣s✱ ✇❤✐❝❤ ♦❢t❡♥ ❛r❡ •❡❢t ✐♠♣•✐❝✐t✳ ❆s s✉❝❤✱ t❤✐s ❢♦r♠❛•✐s♠ ❝❛♥ ❜❡ s❡❡♥ ❛s ❛♥ ✐♥♥♦✈❛t✐✈❡ ❝♦♥tr✐❜✉t✐♦♥ t♦ t❤❡ s❡♠❛♥t✐❝s ♦❢ ♣r♦♦❢ s②st❡♠s✳ ✻✳✷ Pr♦♦❢ r❡✇r✐t✐♥❣ str❛t❡❣✐❡s ❚❤❡ ♥❡❡❞ ❢♦r t❤❡ ❝r❡❛t✐♦♥ ♦❢ ❛ ♠❡❝❤❛♥✐s♠ ❢♦r ♣r♦♦❢ str❛t❡❣✐❡s ✇❛s ❛❝❦♥♦✇•✲ ❡❞❣❡❞ ❛•♦♥❣✇✐t❤ t❤❡ ✜rst t❤❡♦r❡♠ ♣r♦✈❡rs ✐♠♣•❡♠❡♥t❛t✐♦♥s✳ ■♥ ❬✷✻(✱ t❤❡ ❛✉t❤♦rs r❡♠❛r❦ t❤❛t t❤❡✐r ✐♥✐t✐❛• ❛tt❡♠♣ts ❛t ✉s✐♥❣ •❝❢ ❬✹✻(✱ ♦♥❡ ♦❢ t❤❡ ✜rst ❞❡❞✉❝t✐♦♥ s♦❢t✇❛r❡✱ ✇❡r❡ ✏•✐♠✐t❡❞ ❜② t❤❡ ✜①❡❞✱ ❛♥❞ r❛t❤❡r ♣r✐♠✐t✐✈❡✱ ♥❛t✉r❡ ♦❢ ✐ts r❡♣❡rt♦✐r❡ ♦❢ ❝♦♠♠❛♥❞s✑✱


Qui suis-je ? Architecture interne

• Un thread de rendu appelé "audio thread" est seul en charge du rendu sonore du graphe audio ○ Contraintes temps réel fortes : thread de haute priorité. Si il ne parvient pas à fournir le prochain bloc d'échantillons sonores à temps : glitches, dropouts etc.

• Un thread de contrôle, exécutant en général du code JavaScript code pour la GUI, fait les appels à l'API WebAudio, gère la création et modification du graphe audio.

○ connexion/déconnexion des noeuds, modifications de leurs paramètres.

• Les noeuds "standards" traitent le son dans l'audio thread ○ Les algorithmes DSP sont fixes, seuls les paramètres peuvent être modifiés.

• Le noeud

•

  Professeur à l'Université Côte d'Azur (UCA), France ○ Membre de l'équipe WIMMICS commune à INRIA et au laboratoire I3S du CNRS ○ W3C Advisory Committee Representative pour UCA ○ Membre du W3C WebAudio WorkingGroup depuis 2014 ○ michel.buffa@univ-cotedazur.fr, @micbuffa • Membre du groupe qui a créé les Web Audio Modules aka "Plugins audio pour la plateforme Web" (gain1).connect(ctx.destination);

  AudioWorklet (2018) fournit une solution pour implémenter des traitements DSP personnalisés dans l'audio thread. WAM-Studio: un DAW open source compatible WAM ! https://wam-studio.i3s.univ-cotedazur.concevoir un framework host/plugin Web Challenge 2 : host/plugin communication (i.e 44.1Khz) Contrôle bas-niveau de la lecture nécessaire. Chaque piste est un AudioWorklet (WAMNode+WAMProcessor) • Le processeur d'une piste communique avec les plugins à la fréquence d'échantillonnage (WAM SDK) sans quitter le thread audio ! ○ Automation des paramètres : DEMO ○ Envoyer des notes MIDI : DEMO No need to schedule ahead in time like in the famous article "A tale of two clocks" by C.Wilson.

Challenge 3 : gérer la latence Latence = RETARD ! 1 -Latency Round-trip: la durée qu'il faut pour qu'un signal, tel qu'une voix chantée ou un solo de guitare, passe d'une entrée analogique sur une interface audio, à travers les convertisseurs analogique-numérique, jusqu'au DAW, puis retourne ressorte par l'interface audio. Si cette durée est élevée, cela impacte négativement la capacité du musicien à jouer en rythme, par exemple. Elle devrait être < 20 ms.

-


main or audio thread 1 -The WebAudioModule API Main Thread Host

Concepts de l'API WebAudio

The Web Audio API also supports custom DSP programming with the AudioWorklet This is where custom DSP processing is done! Can be done in JavaScript or in a WebAssembly module! This is where the AW node is created, connected to the audio graph, where the GUI is managed etc. (JavaScript)

Web Audio development

Web developers

• Use plain HTML/CSS/JavaScript but very often also bundlers/minifiers (webpack, parcel, rollup), npm modules, frameworks (react, vueJS), and also code with TypeScript, etc.

Audio developers

• Use C++/Rust, DSLs like FAUST, Csound, CMajor, patchers like Max, etc. • Use plugin standards: VSTs, AU, AAX, RTAS, JUCE, CLAP, iPlug2, etc.

How to combine all this? WebAudioModules version 2 (aka WAM or WAM2) Used by the community to publish and share "ready to use" plugins!

• Remember that a plugin is just a URI! • Several dozens of plugins available, 99% also available with source code to study (github.com/boourns/burns-audio-wam) • Cover all classic effects, proposes some instruments and utilitary plugins. • All plugins available in the https://sequencer.party host.

FAUST: a DSL for DSP programming, born in 2002 at GRAME-CNCM, France

Used in artistic productions, education and research, open source projects and commercial applications.

Faust offers end-users a high-level alternative to C/C++ to develop audio applications for a large variety of platforms.

The role of the Faust compiler is to synthesize the most efficient implementations for the target language (C, C++, LLVM, WebAssembly, etc.).

Online doc / tutorial so that you can experiment yourself, create, build GUI, export WAM2 plugins directly from the FAUST online IDE.

Conclusion / Perspectives

The WAM standard is stable now and comes with many examples. -the role of processes seems to assume more importance than their results -the notions of non-linearity and erraticism have increasingly become part of creative processes -digital creativity : digital objects can be modified by human-computer interaction more than ever, and that the formal connotations of a musical work may be re-tracked in an ever-changing way -the interpretation of sonorous events has to deal with dynamism of inter-medial relationships -relationships between musical subjectivity and the emotional indexes of sonorous space ¤ Moles (1972): the object is situated at the crossroads of an interaction when there is a conjunction between situation and act, so it is always included in a praxeological dimension.

Device and creativity

Agamben (2014): "I call a device (p.31) anything that has, in one way or another, the capacity to capture, orientate, determine, intercept, model, control and ensure the gestures, conducts, opinions and discourses of living beings."

-The device ranges from the school to the pen, from the asylum to the cell phone.

-Foucault has thus shown how, in a disciplinary society, devices aim, through a series of practices and discourses, knowledge and exercises, to create docile yet free bodies that assume their identity and freedom as subjects in the very process of their subjection.

-The device is therefore, above all, a machine that produces subjectivation. Digital Creativity is a constant negotiation between the engagement in a NMP process or WAM interaction, non linear music production, and the freedom of music agency and literacy, in which serendipity could have a central role.

  (gain1).connect(ctx.destination);

•

  Developers can choose to adapt their existing code to the API • Others can use the SDK that implements the API (much easier), inherit classes etc. available at https://wam-examples.vidalmazuy.fr/ Also, check the wam-community repository https://github.com/boourns/wam-community

  OUR MAIN CONCERN NOW: grow adoption, more users, more developers! Things that will come soon: ○ The wam-community repo is growing every week :-) ○ The WAM SDK has been extended to support 3D WebGL/GLSL/Video extensions ○ A WAM based DAW has been released and is open source ○ More examples for developers: using WASM, in particular C++/WASM ○ Remote plugin server with API Join us on slack WebAudio channel / #webaudiomodules! • Renwick, Robin. (2012). "SOURCENODE: A NETWORK SOURCED APPROACH TO NETWORK MUSIC PERFORMANCE (NMP).hdl:2027/spo.bbp2372.2012.057. David Kim-Boyle (2009) Network Musics: Play, Engagement and the Democratization of Performance,Contemporary Music Review, 28:4-5, 363-375, DOI: 10.1080/07494460903422198 "the strategies employed in the work of these artists have helped redefine a new aesthetics of engagement in which play, spatial and temporal dislocation are amongst the genre's defining characteristics". digital creativity Tanzi, D. (2005) -'Musical objects and digital domains'. Proceedings of EMS-05 Conference. Montreal, Quebec, October 19-22, 2005

  parameter info for the specified parameter ids, or omit argument to get info for all parameters. */ getParameterInfo(...parameterIdQuery: string[]): Promise<WamParameterInfoMap>; /** Get parameter values for the specified parameter ids, or omit argument to get values for all parameters. */ getParameterValues(normalized?: boolean, ...parameterIdQuery: string[]): Promise<WamParameterDataMap>; /** Set parameter values for the specified parameter ids. */ setParameterValues(parameterValues: WamParameterDataMap): Promise<void>; /** Returns an object (such as JSON or a serialized blob) that can be used to restore the WAM's state. a callback function so it will be called when matching events are processed. */ addEventListener<K extends keyof WamEventMap>(type: K, listener: (this: this, ev: CustomEvent<WamEventMap[K]>) => any, options?: boolean | AddEventListenerOptions): void; addEventListener(type: string, listener: (this: this, ev: CustomEvent) => any, options?: boolean | AddEventListenerOptions): void; addEventListener(type: string, listener: EventListenerOrEventListenerObject, options?: boolean | AddEventListenerOptions): void; /** Deregister a callback function so it will no longer be called when matching events are processed. */ removeEventListener<K extends keyof WamEventMap>(type: K, listener: (this: this, ev: CustomEvent<WamEventMap[K]>) => any, options?: boolean | EventListenerOptions): void; removeEventListener(type: string, listener: (this: this, ev: CustomEvent) => any, options?: boolean | AddEventListenerOptions): void; removeEventListener(type: string, listener: EventListenerOrEventListenerObject, options?: boolean | EventListenerOptions): void; /** Schedule a WamEvent. Listeners will be triggered when the event is processed. an event output stream to another WAM. If no output index is given, assume output 0. */ connectEvents(to: WamNode, output?: number): void; /** Disconnect an event output stream from another WAM. If no arguments are given, all event streams will be disconnected. */ disconnectEvents(to?: WamNode, output?: number): void; /** Stop processing and remove the node from the graph. Stop processing and remove the node from the WAM event graph. */ destroy(): void; } WamEnv and WamGroup: manage plugin chains Send events downstream to a list of chained plugins…, manage group (states) etc.

The official github repo is the regular webaudiomodules one: https://github.com/webaudiomodules.

	○	A WAM plugin can be loaded using a
		simple URI!
	○	A WAM plugin is a JavaScript module,
	○ (2015), and WAM2 is the updated version: A WAM can be made of a single
		AudioWorklet Node, or made of multiple
	nodes, it will behave like a single • webaudiomodules.org will remain the home
	AudioNode. Plugin parameters are handled by the WamParamMgr, of the project (not yet up to date! ○ How to start with WAMs! Soon with a section about WAM2!)
	○ ○ ○ ○ ○ • • Everything is under MIT/MPL/Apache 2.0 Focus on performance (ring buffer, audio thread isolation) Plain modern JS or build systems for JS / TS / frameworks Support for C/C++ Support for DSL (Faust, CSound) Parameter Automation, MIDI support, ○ open source licence… host/plugin interaction as an API (+ rich SDK). The API can be entirely • Also available as npm modules
		re-implemented for low-level plugins

• 2021-2022: WebAudio Modules 2.0

WebAudioModules (WAM) is an old standard

WebAudioModule API WamNode API AudioWorklet Thread Host WamProcessor API WamEnv API GUI will return true after calling `initialize()`. */ initialized: boolean; /** The identifier of the current WAM, composed of vender + name */ readonly moduleId: string; /** The unique identifier of the current WAM instance. */ readonly instanceId: string; /** The values from `descriptor.json` */ readonly descriptor: WamDescriptor; /** The WAM's name */ readonly name: string; /** The WAM Vendor's name */ readonly vendor: string; /** * This async method must be redefined to get `AudioNode` that * will connected to the host. * It can be any object that extends `AudioNode` and implements `WamNode` The WAM devs can also fetch and preload the GUI Element in while initializing. Redefine this method to get the WAM's GUI as an HTML `Element`. */ createGui(): Promise<Element>; /** Clean up an element previously returned by