Transcript Adjunct Elimination in Context Logic for Trees

Adjunct Elimination in
Context Logic for Trees
Cristiano Calcagno
Thomas Dinsdale-Young
Philippa Gardner
Imperial College, London
Context Logic
• Ambient Logic (Cardelli, Gordon) is a logic for
reasoning about static properties of nodelabelled, unranked trees (e.g. Firewalls, XML
data)
• Separation Logic (O’Hearn, Reynolds, Yang) is a
logic for local reasoning about dynamic heap
update
• Context Logic evolved from these two as a logic
for local reasoning about dynamic tree update
– Talks both about trees and contexts into which they
may be placed
u[P]
P1 | P2
K(P)
KP
P1  P2
Adjoints
• The adjoints allow us to reason
hypothetically about an extended object
• They are essential for expressing weakest
preconditions
• But for closed formulae, the adjoints add
no expressive power to Separation Logic
(Lozes) and Ambient Logic (Lozes, and
later Dawar, Gardner, Ghelli)
Adjunct Elimination
• Intuition:
– adjoints make us reason about trees that are
bigger than the ones we are actually
interested in
– we would expect that any property expressed
in terms of these hypothetical trees could be
expressed without them
• In Context Logic for Trees, one of the
adjoints () can also be eliminated, but
the other () cannot (Dinsdale-Young)
Non-eliminability of 
• Trees can be split arbitrarily into a context and subtree
• Using , we can fill the context hole and then split it as a
tree
• We cannot split an arbitrary subtree (or subcontext) from
a context
Counterexample
• The formula 0 True(u[0])
– Expresses “putting the
empty tree into the context
hole gives a tree that has a
leaf u”
– Distinguishes ci from di for
all i
• There is no formula
without adjoints that can
express this property
ci
di
u
u
u
u
i times
u
u
u
v
Context Logic with Composition
• Adding context
composition “fixes”
the counterexample –
we can now split
contexts
• Not yet proved
adjunct elimination
• Still can’t split
contexts in the same
way as trees
y
x
Multi-holed Context Logic for
Trees
Ehrenfeucht-Fraïssé Games
• We prove adjunct elimination using ranked games
–
–
–
–
Played between Spoiler and Duplicator
On two tree contexts
Moves correspond with logical connectives
Rank determines which moves may be played and ensures
termination
• Spoiler’s aim is to demonstrate a difference between the
two trees. Duplicator’s aim is to prevent this.
• The games are sound and complete: Spoiler has a
winning strategy if and only if the trees can be
distinguished by a formula of the game rank (of which
there are finitely many)
Games
non-adjunct
moves
adjunct
moves
node
labels
((c, σ), (c', σ'), (n, s, L))
tree context
rank
environment
• Spoiler starts each round by choosing a move
to play (providing that the rank and rules allow it)
and one of the context-environment pairs
• The rules for the move determine what happens
Game Moves
CMP move
c
c'
x
α
β
x
z
σ
α
β
y
x
σ'
CMP move
c
c'
x
α
β
x
z
σ
α
β
y
x
σ'
CMP move
c
c'
x
α
β
x
z
σ
α
β
y
x
σ'
CMP move
c 1'
c
y
x
c 2'
α
β
x
z
σ
α
β
y
x
σ'
CMP move
c1
c 1'
x
y
x
c2
α
β
c 2'
x
z
σ
α
β
y
x
σ'
CMP move
c2
c 2'
α
β
x
z
σ
α
β
y
x
σ'
Game Moves
RIG move
c
c'
x
y
x
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c
c'
x
y
x
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c
c'
x
y
x
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c2=c x c1
c'
y
x
c1
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c2=c x c1
c2'=c' y c1'
x
α
β
σ
c1
c 1'
x
z
α
β
y
x
σ'
RIG move
c2
c2'
x
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c
c'
x
y
x
α
β
x
z
σ
α
β
y
x
σ'
RIG move
c
c'
x
y
x
α
β
x
z
σ
α
β
y
x
σ'
Adjunct Elimination
• We prove that whenever Spoiler has a
winning strategy using adjunct moves he
also has one without using adjunct moves
• By soundness and completeness of
games, this implies adjunct elimination
Key Result
• We need to show:
If Duplicator can win when Spoiler plays no
adjunct moves then Duplicator can also win
when Spoiler plays adjunct moves
• We show how Duplicator responds to one
adjunct move (LEF or RIG)
• The result follows by induction
»
»
»
»
Key Result
Proof
• The proof is by induction on n
• We look at the cases for which move
Spoiler plays on the composite game
• Some cases have sub-cases
• Example: CMP move
c=c1 x c2
CMP move
(case 1)
CMP move
(case 2)
CMP move
(case 3)
CMP move
(case 4)
CMP move
(case 1)
c=c1 x c2
c'=c1' x c2'
CMP move
(case 1)
?
CMP move
(case 1)
»
3n
c2
c2'
CMP move
(case 1)
»
3n-1
»
3n-1
CMP move
(case 1)
»
3(n-1)
x
x
y
»
3(n-1)
y
CMP move
(case 1)
»
n-1
y
y
CMP move
(case 1)
»
n-1
y
y
»
n-1
Related and Further Work
• Without adjuncts, Context Logic formulae can be
expressed by regular forest grammars
• Heuter and Bojańczyk have studied similar classes of
regular languages that correspond to definability in FirstOrder Logic
• Automata may give a decision procedure for multi-holed
Context Logic with adjoints
• Multi-holed Context Logic may prove useful for
concurrent tree update
• Calcagno, Gardner and Zarfaty have shown that adjunct
elimination does not hold on open formulae (i.e. with
propositional variables)
Conclusions
• Adjunct elimination does not hold for
single-holed Context Logic for trees
• Multi-holed Context Logic is a natural
extension of the single-holed logic
• Adjunct elimination does hold for this logic
As the poet said, ‘Only God can make a tree’ –
probably because it’s so hard to figure out how to get the bark on.
– Woody Allen
Satisfaction Relation