Higher-Order Semantic Labelling forInductive Datatype Systems

Makoto Hamana
Gunma University/University of TokyoJapanPPDP’07
14th July, 2007.
1

Intro: Termination Proof by Syntactic Method
Term Rewriting System (TRS) R:
f act(s(x)) → f act(x) ∗ s(x)B Recursive path ordering (RPO) [Dershowitz TCS’82]
proves termination (= SN) by using the precedence
f act > ∗ > s > 02

Intro: Semantic Labelling for TRSs [Zantema’95]
Original TRS R:
f act(s(x)) → f act(p(s(x))) ∗ s(x)p(s(0)) → 0p(s(s(x))) → s(p(s(x)))
I RPO doesn’t work
Semantics: Σ-algebra (N, {f actN , sN , pN : N → N, · · ·})Labelled TRS R:
f acti+1 (s(x)) → f acti (p(s(x))) ∗ s(x)p(s(0)) → 0p(s(s(x))) → s(p(s(x)))
I RPO works!
Th. [Zantema’95] TRS R is terminating3⇒

R is terminating.

This Work
B About higher-order term rewriting
B Inductive Data Type Systems (IDTSs)& Termination criteria: the General Schema[Blanqui,Jouannaud,Okada TCS’02, RTA’00]
B Diﬃculty:

what is a suitable semantic structure forlabelling higher-order rewriting systems?

B Contribution:i. Answerii. Higher-order semantics labellingiii. Applications

4

Inductive Data Type Systems[Blanqui,Jouannaud,Okada RTA’00, TCS’02]
Features:
B Rewrite rules on higher-order terms
B Simple types (up to 2nd-order in this work)
B Inductive types (by conditions of types of constructors)
B Metavariables with arities and substitutions, e.g.
ap(λ(x.M (x)), N ) → M (N )5

Idea: Attach Semantics of Arguments in Rewrite Rules
Original R

f (l) → g(· · · f (t) · · ·)⇓Labelled Rf[[l]]ρ (l0 ) → g(· · · f[[t]]ρ (t0 ) · · ·)(M, ≥) : quasi-model
ρ:X →M(∀(l → r) ∈ R. [[l]]ρ ≥ [[r]]ρ)valuation[[−]] : TΣ X → M

6What Kind of Semantics for Higher-Order Labelling?
B TRS: (1st-order) Universal algebra
B IDTS: ?? Higher-order version of universal algebra
B Semantics of Higher-order Rewrite Systems by van de Pol[HOA’93]: hereditary monotone functionals,
but not complete for termination.
The term model is not a model.
B Need to satisfy several requirements

7

What Kind of Semantics for Higher-Order Labelling?
s →R tSemantic labels must reﬂect:
B contexts00g[[s]] ( s ) →R g[[t]] ( t )B binders00

λ[[s]]x (x. s ) →R λ[[t]]x (x. t )B substitutions
map(x.F (x), cons(M, N )) →R cons(F (M ), · · ·)⇓· · · →R cons[[F ]][[M ]] (F (M ), · · ·)8

What Kind of Semantics for Higher-Order Labelling?
B Models of λ-calculus?
B But λ-algebra doesn’t satisfy ξ-rule in general [Plotkin JSL’74]
M =N
λx.M = λx.N
B Right framework: binding algebras and Σ-monoids[Fiore,Plotkin,Turi LICS’99] with order structure
B Σ-monoid = Σ-algebra + monoid
B Free Σ-monoid = higher-order syntax with metavariables[Hamana APLAS’04]
B Algebraic semantics of higher-order rewriting [Hamana RTA’05]
B Typed binding algebra [Fiore PPDP’02]
9Semantic Labelling
B An assignment φ : Z- M into a quasi-model-M ZΣB Labelling map φL : MΣ ZLφ (x) = xLLφ (z(~t)) = z(φ ~t)
LLLφ (f (t1 , . . . , tl )) = fhhφ∗ (t1 ),...,φ∗ (tl )iif (φ t1 , . . . , φ tl )B LabellingFree Σ-monoid
Σ-m.m.
Σ-monoidterms

l→r∈RMΣ Z

labelling map φLlabelled terms

?

MΣ Z?
LL

φ (l) → φ (r) ∈ Rlabelled IDTS

10

Higher-Order Semantic Labelling
B Proposition
termslabelling map φLlabelled terms

s →R tMΣ 0?

MΣ 0L

∗?

B Th. [Higher-order semantic labelling]
IDTS R ∪ Decr is terminating ⇒ R is terminating.

B “Decreasing rules” Decr
fp (z1 , . . . , zl ) → fq (z1 , . . . , zl )for all labels p > q11

Lφ (s) →Decr· →R φ (t)Application 1: Simply-Typed λx-calculus [Bloo,Rose’95](λx.M )N → M hx := N i(M N )hx := Ki → M hx := Ki N hx := Ki(λy.M )hx := Ki → λy.M hx := Ki

if x 6= yxhx := Ki → K
M hx := Ki → M

if x 6∈ FV(M )B This doesn’t follow the General Schema:??

@ > −h− := −i− h− := −i > @B Labels help!
Semantics · · · simply typed λ-terms evaluating all ex. subst.

12

Application 1: Simply-Typed λx-calculus(λx.M )N → M hx := N i(M N )hx := Ki → M hx := Ki N hx := Ki(λy.M )hx := Ki → λy.M hx := Ki

if x 6= yxhx := Ki → K
M hx := Ki → M

if x 6∈ FV(M )B Labelled rules
ap(λx.s)t (λ(x.M (x)), N ) → M (x)hx := N is[x:=t](aps t (M (x), N (x)))hx := Kist[x:=u] → apst[x:=u] (· · ·)Precedence: aps > −h− := −it > apt > λfor s (→β ∪ B )∗ tB This follows the General Schema, hence SN
B Point: λ-terms form a quasi-model of λx-calculus
B NB. Not a termination model (i.e. not giving ’>’) but useful13

Application 2: Labelling with Term Model
B Example: λx-calculus
B (Restricted) term model is a typical model
B Take the full term model (TΣV, (→R ∪ B )∗ )Def. [Middeldorp,Ohsaki,Zantema CADE’96]
A 1st-order TRS R is precedence terminating
if ∃ well-founded order (“precedence”) s.t.
f (~t) → r ∈ R, f > ∀g ∈ Fun(r)Prop. R SN

⇔term labelled R ∪ Decr precedence terminating

B TRS ok [MOZ’96]
B IDTS fails – subterm property is not closed under substitutions
B Solid IDTS oknew notion
14

Solid IDTS
Def. A term t is solid
if for each z(s1 , . . . , sn ) in t,.
all si do not contain function symbols
Def. IDTS R is solid if
i. R consists of solid terms onlyii. (about strictly positive inductive types and accessibility of variables)
Examplei. ap(λ(x.M (x)), N ) → M (N )ii. λx-calculus
Prop. Solid IDTS R SN⇔

R ∪ Decr precedence terminating

15

Application 3: Modularity with HO-RPS
HO Recursive Program Schema (RPS)f (x1 . . . xi1 .z1 (x1 , . . . , xi1 ), . . .) → t
Th. Termination is modular for the disjoint union ofsolid IDTS and solid HO-RPS.
Proof Labelling with a term model given by normal forms ofHO-RPS and show precedence termination.

16

SummaryB Higher-order semantic labelling for IDTSs using Σ-monoids
B Applications: λx, modularity
B Introduction of solid property- Reasonable extension of FO case
NoteB Almost no property is modular for HO rewriting [van Oostrom’05]
B Signature extension doesn’t preserve SN for HO rewriting
B But solid case is ok17

Why fails?
B Consider labelling with a term model
B Need to establish the propertyf (l) → r ∈ R
ff (l)θ (l) → r ∈ R
f (l)θ →R rθ D tθfor r D t

Take the order on labels: (→R ∪ B )∗- TRS ok- IDTS NG, sincez(f ) B f⇒

c 6B f18

by z 7→ cΣ-monoids [Fiore,Plotkin,Turi’99]
A Σ-monoid consists of
B a monoid object M = (M, η, µ)in the monoidal category (SetF , •, V) (“substitution prod.”) with
B a Σ-binding algebra α : ΣM → M such that
Σ(M ) • M

st- Σ(M • M )α•MΣµ- ΣM

α?

?

M •M

µcommutes.

19-M