|
%%-------------------** Term Rewriting System (TRS) **------------------------
%%
%% Authors : Ana Cristina Rocha Oliveira, Andre Galdino and Mauricio Ayala Rincon
%% Universidade de Brasília - Brasil
%% Orthogonality theory formalizing confluence of orthogonal rewriting systems
%% subtheories mem_test and mem_tes2 specify properties between finite sequences
%% and associated sets that are necessary for dealing adequately with sequences
%% of positions, rules and substitutions involved in parallel rewriting steps.
%% The theory orthogonality is the main one.
%%
%% Last Modified On: June 28, 2013
%%
%%--------------------------------------------------------------------------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% mem_test is an auxiliary theory formalising properties related with length and
%% cardinality and membership of elements in finite_sequences and associated sets.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
mem_test[T: TYPE] : THEORY
BEGIN
IMPORTING structures@seq_extras[T],
structures@seq2set[T]
x : VAR T
seq, seq1, seq2: VAR finseq[T]
E : VAR set[T]
n : VAR nat
P : VAR [[T, T] -> bool]
P1 : VAR [[nat, T] -> bool]
member_seq(x, seq): bool =
EXISTS(i:below[seq`length]): x = seq(i)
subseq(seq1, seq2): bool =
FORALL(i:below[seq1`length]): member_seq(seq1(i),seq2)
member(seq, E): bool = FORALL(i:below[seq`length]):
member(seq`seq(i),E)
power(x,n): finseq[T] =
(# length := n,
seq := (LAMBDA(i:below[n]): x) #)
member_seq_in_seq2set: LEMMA
member_seq(x, seq) IFF seq2set(seq)(x)
subseq_rest: LEMMA
subseq(seq1, rest(seq2)) IMPLIES subseq(seq1, seq2)
seq2set_comp: LEMMA
seq2set(seq1 o seq2)(x)
IFF seq2set(seq1)(x) OR seq2set(seq2)(x)
seq_construct: LEMMA
seq1`length = n &
seq2`length = n &
(FORALL (i:below[n]):
EXISTS x: P(seq1`seq(i), x) &
P(seq2`seq(i), x))
IMPLIES EXISTS seq: seq`length = n &
FORALL (i:below[n]):
P(seq1`seq(i), seq`seq(i)) &
P(seq2`seq(i), seq`seq(i))
seq_construct2: LEMMA
(FORALL (i:below[n]):
EXISTS x: P1(i, x))
IMPLIES EXISTS seq: seq`length = n &
FORALL (i:below[n]):
P1(i, seq`seq(i))
END mem_test
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Orthogonality contains specification of notions related with orthogonal
%% rewriting systems, parallel rewriting and the formalization of theorems
%% of confluence of left and right linear non-ambiguous TRSs and the main
%% theorem of confluence of orthogonal TRSs.
%% The inductive proof of the main theorem uses the Parallel Moves Lemma.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
orthogonality[variable:TYPE+, symbol: TYPE+, arity: [symbol -> nat]]: THEORY
BEGIN
ASSUMING
IMPORTING
variables_term[variable,symbol, arity],
sets_aux@countability[term],
sets_aux@countable_props[term]
var_countable: ASSUMPTION is_countably_infinite(V)
ENDASSUMING
IMPORTING critical_pairs[variable,symbol,arity],
mem_test[term],
mem_test[position],
mem_test[rewrite_rule],
mem_test[Sub]
n: VAR nat
s, t, t1, t2: VAR term
sigma, sg1, sg2, alpha, delta, theta: VAR Sub
p,q,p1,p2,p3,q1,q2: VAR position
rho, rho1, rho2: VAR Ren
e, e1o, e2o, e1, e1p, e2, e2p: VAR rewrite_rule
E: VAR set[rewrite_rule]
R: VAR pred[[term, term]]
x, y: VAR (V)
fsq, fsp, fsp1, fsp2: VAR finseq[position]
fse, fse1, fse2: VAR finseq[rewrite_rule]
fss, fss1, fss2: VAR finseq[Sub]
fsv: VAR finseq[(V)]
fst, fst1, fst2: VAR finseq[term]
PO1, PO2, PE: VAR PP
%%%% Basic specific definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% ntCP? is the predicate for non trivially generated CPs %%%%%%%%%%%%%%%%%%%%%%%%
%%%%% This in contrast with CP? excludes all CPs generated by sobreposition of %%%%%%
%%%%% a rule with itself at root position and is used to define ambiguity. %%%%%%
%%%%% The necessity of this notion was gently pointed out by Rene Thiemann. %%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ntCP?(E)(t1, t2): bool =
EXISTS (sigma,rho,
(e1 | member(e1, E)),
(e2p | member(e2p, E)),
(p: positions?(lhs(e1)))):
NOT (e1 = e2p AND p = empty_seq) AND
LET e2 = (# lhs := ext(rho)(lhs(e2p)), rhs := ext(rho)(rhs(e2p)) #) IN
disjoint?(Vars(lhs(e1)),Vars(lhs(e2))) &
NOT vars?(subtermOF(lhs(e1), p)) &
mgu(sigma)(subtermOF(lhs(e1), p), lhs(e2)) &
t1 = ext(sigma)(rhs(e1)) &
t2 = replaceTerm(ext(sigma)(lhs(e1)), ext(sigma)(rhs(e2)), p)
ntCP_lemma_aux1: LEMMA
FORALL E, (p: position), (e1 | member(e1, E)), (e2 | member(e2, E)):
( ( positionsOF(lhs(e1))(p) &
NOT vars?(subtermOF(lhs(e1), p)) &
ext(sg1)(subtermOF(lhs(e1), p)) = ext(sg2)(lhs(e2)) ) &
NOT (e1 = e2 AND p = empty_seq) )
=>
EXISTS t1, t2, delta:
ntCP?(E)(t1, t2) &
ext(delta)(t1) = ext(sg1)(rhs(e1)) &
ext(delta)(t2) = replaceTerm(ext(sg1)(lhs(e1)), ext(sg2)(rhs(e2)), p)
Ambiguous?(E): bool = EXISTS (t1, t2) : ntCP?(E)(t1,t2)
linear?(t): bool = FORALL (x | member(x,Vars(t))) : Card[position](Pos_var(t,x)) = 1
Right_Linear?(E): bool = FORALL (e1 | member(e1, E)) : linear?(rhs(e1))
Left_Linear?(E): bool = FORALL (e1 | member(e1, E)) : linear?(lhs(e1))
Linear?(E): bool = Left_Linear?(E) AND Right_Linear?(E)
local_joinability_triangle?(R) : bool = FORALL(t, t1, t2) : R(t, t1) & R(t, t2) =>
EXISTS s : (RC(R)(t1, s) & RC(R)(t2, s))
%%%% Some Lemmas %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Orth_lemma_aux0 : LEMMA
Card(Pos_var(t, x)) = 1 => EXISTS (p1) : (positionsOF(t)(p1) AND subtermOF(t,p1) = x )
equality_replaceTerm : LEMMA
positionsOF(s)(p) =>
(t1 = t2 iff replaceTerm(s, t1, p) = replaceTerm(s, t2, p))
Var_occurs_only_once_also_in_subterms : LEMMA
vars?(x) & positionsOF(s)(p) & p`length /= 0 &
x = subtermOF(s, p) &
card(Pos_var(s,x)) = 1 =>
card(Pos_var(subtermOF(s, #(first(p))),x)) = 1
SigmaP_equivalence : LEMMA
(NOT member(x, Vars(s)) &
positionsOF(ext(sigma)(x))(p2))
=> ext(SigmaP(sigma, t, x, p2))(s) = ext(sigma)(s)
SigmaP_vs_replaceTerm_linearR : LEMMA
vars?(x) & positionsOF(s)(p1) &
positionsOF(ext(sigma)(x))(p2) &
x = subtermOF(s, p1) &
Card(Pos_var(s,x)) = 1 =>
ext(SigmaP(sigma, t, x, p2))(s) =
replaceTerm( ext(sigma)(s), t, p1 o p2)
Orth_lemma_aux: LEMMA
LET e1o = (# lhs := ext(rho1)(lhs(e1p)), rhs := ext(rho1)(rhs(e1p)) #) IN
LET e2o = (# lhs := ext(rho2)(lhs(e2p)), rhs := ext(rho2)(rhs(e2p)) #) IN
member(e1p,E) &
member(e2p,E) &
positionsOF(t)(p1) &
positionsOF(t)(p3) &
NOT Ambiguous?(E) &
p3 = p1 o p2 &
Linear?(E) &
subtermOF(t, p1) = ext(sg1)(lhs(e1o)) &
t1 = replaceTerm(t, ext(sg1)(rhs(e1o)), p1) &
subtermOF(t, p3) = ext(sg2)(lhs(e2o)) &
t2 = replaceTerm(t, ext(sg2)(rhs(e2o)), p3) &
disjoint?(Vars(lhs(e1o)),Vars(t))&
disjoint?(Vars(lhs(e2o)),Vars(t))
=>
EXISTS s: (RC(reduction?(E))(t1, s) & RC(reduction?(E))(t2, s))
Linear_and_Non_ambiguous_implies_triangle: LEMMA
FORALL (E) :
(Linear?(E) AND NOT Ambiguous?(E) ) IMPLIES
local_joinability_triangle?(reduction?(E))
Triangle_implies_conflent: LEMMA
local_joinability_triangle?(R)
IMPLIES confluent?(R)
Linear_and_Non_ambiguous_implies_confluent: LEMMA
FORALL (E) :
((Linear?(E) AND NOT Ambiguous?(E) ) IMPLIES
confluent?(reduction?(E)))
%%%% More definitions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Orthogonal?(E): bool = Left_Linear?(E) & NOT Ambiguous?(E)
Orthogonal: TYPE = (Orthogonal?)
replace_par_pos(s, (fsp : SPP(s)), fst | fst`length = fsp`length): RECURSIVE
term =
IF length(fsp) = 0
THEN
s
ELSE
replace_par_pos(replaceTerm(s, fst(0), fsp(0)), rest(fsp), rest(fst))
ENDIF
MEASURE length(fsp)
reduction_fix?(E)(s,t,(p:positions?(s))): bool =
EXISTS (e|member(e,E), sigma):
subtermOF(s,p)=ext(sigma)(lhs(e))
AND t=replaceTerm(s,ext(sigma)(rhs(e)),p)
sigma_rhs(fss, (fse | fse`length = fss`length)): finseq[term] =
IF fss`length = 0 THEN empty_seq[term]
ELSE
(# length := fss`length,
seq := (LAMBDA (i: below[fss`length]): ext(fss(i))(rhs(fse(i)))) #)
ENDIF
sigma_lhs(fss, (fse | fse`length = fss`length)): finseq[term] =
IF fss`length = 0 THEN empty_seq[term]
ELSE
(# length := fss`length,
seq := (LAMBDA (i: below[fss`length]): ext(fss(i))(lhs(fse(i)))) #)
ENDIF
subtermsOF(t,(fsp:SP(t))):
finseq[term] = (# length := fsp`length,
seq := (LAMBDA (i: below[fsp`length]): subtermOF(t,fsp(i))) #);
parallel_reduction_fix?(E)(s,t, (fsp: SPP(s))): bool =
EXISTS ((fse | member(fse, E)), fss) :
fsp`length = fse`length AND fsp`length = fss`length
AND subtermsOF(s,fsp) = sigma_lhs(fss, fse)
AND t = replace_par_pos(s, fsp, sigma_rhs(fss, fse))
parallel_reduction?(E)(s,t): bool = EXISTS (fsp: SPP(s)): parallel_reduction_fix?(E)(s,t,fsp)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sub_pos((fsp : PP), p): RECURSIVE finseq[position] =
IF length(fsp) = 0 THEN empty_seq[position]
ELSIF p <= fsp`seq(0) AND p /= fsp`seq(0)
THEN add_first(fsp`seq(0), sub_pos(rest(fsp), p))
ELSE sub_pos(rest(fsp), p)
ENDIF
MEASURE length(fsp)
% Positions of fsp1 that have positions of fsp2 strictly below or are parallel to fsp2
Pos_Over((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
(IF length(fsp1) = 0
THEN empty_seq[position]
ELSE (IF ( length(sub_pos(fsp2, fsp1`seq(0))) > 0
OR PP?(add_first(fsp1`seq(0), fsp2)))
THEN add_first(fsp1`seq(0), Pos_Over(rest(fsp1), fsp2))
ELSE Pos_Over(rest(fsp1), fsp2)
ENDIF)
ENDIF)
MEASURE length(fsp1)
% Positions of fsp1 that are strictly below some position of fsp2.
Pos_Under((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
IF length(fsp2)=0
THEN empty_seq[position]
ELSE sub_pos(fsp1, fsp2`seq(0)) o Pos_Under(fsp1,rest(fsp2))
ENDIF
MEASURE length(fsp2)
% Positions of fsp1 and fsp2
Pos_Equal((fsp1 : PP), (fsp2 : PP)): RECURSIVE finseq[position] =
IF length(fsp1) = 0 THEN empty_seq[position]
ELSIF member_seq(fsp1`seq(0),fsp2)
THEN add_first(fsp1`seq(0), Pos_Equal(rest(fsp1), fsp2))
ELSE Pos_Equal(rest(fsp1), fsp2)
ENDIF
MEASURE length(fsp1)
%%%% Lemmas about parallel reduction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
comp_SPP_commute: LEMMA
SPP?(s)(fsp1 o fsp2) IMPLIES SPP?(s)(fsp2 o fsp1)
sub_pos_element: LEMMA
PP?(fsp) & member_seq(p1 o p2, fsp) & p2`length /= 0
IMPLIES sub_pos(fsp, p1)`length /= 0 &
member_seq(p1 o p2, sub_pos(fsp, p1))
parallel_pos_are_dif: LEMMA
PP?(fsp) IMPLIES FORALL(i,j: below[fsp`length]): i /= j => fsp(i) /= fsp(j)
same_pos_in_Pos_Equal: LEMMA
PP?(fsp1) & PP?(fsp2) & member_seq(p, fsp1) & member_seq(p, fsp2)
IMPLIES member_seq(p, Pos_Equal(fsp1, fsp2))
Pos_Over_is_sub_seq: LEMMA
PP?(fsp1) & PP?(fsp2)
IMPLIES subseq(Pos_Over(fsp1,fsp2), fsp1)
Pos_Equal_is_sub_seq: LEMMA
PP?(fsp1) & PP?(fsp2)
IMPLIES subseq(Pos_Equal(fsp1,fsp2),fsp1)
sub_pos_is_sub_seq: LEMMA
PP?(fsp) IMPLIES subseq(sub_pos(fsp,p), fsp)
Pos_Under_is_sub_seq: LEMMA
PP?(fsp1) & PP?(fsp2)
IMPLIES subseq(Pos_Under(fsp1,fsp2), fsp1)
Pos_Over_is_PP: LEMMA
PP?(fsp1) & PP?(fsp2) IMPLIES
PP?(Pos_Over(fsp1, fsp2))
Pos_Over_is_SPP: LEMMA
SPP?(s)(fsp1) & SPP?(s)(fsp2) IMPLIES
SPP?(s)(Pos_Over(fsp1, fsp2))
pos_up_in_Pos_Over: LEMMA
PP?(fsp1) & PP?(fsp2) &
p2`length /= 0 & member_seq(p1, fsp1) & member_seq(p1 o p2, fsp2)
IMPLIES member_seq(p1, Pos_Over(fsp1, fsp2))
parallel_pos_in_Pos_Over: LEMMA
PP?(fsp1) & PP?(fsp2) & member_seq(p, fsp1) & PP?(add_first(p, fsp2))
IMPLIES member_seq(p, Pos_Over(fsp1, fsp2))
sub_pos_in_Pos_Under_aux: LEMMA
PP?(fsp) & member_seq(p2, fsp) &
p1 /= p2 & p1 <= p2 IMPLIES
member_seq(p2, sub_pos(fsp,p1))
sub_pos_in_Pos_Under: LEMMA
PP?(fsp1) & PP?(fsp2) & member_seq(p1, fsp1) &
member_seq(p2, fsp2) & p1 /= p2 & p2 <= p1 IMPLIES
member_seq(p1, Pos_Under(fsp1, fsp2))
sub_pos_is_under: LEMMA
PP?(fsp) & member_seq(p1, sub_pos(fsp,p))
IMPLIES p<=p1 & p/=p1
sub_pos_is_PP: LEMMA
PP?(fsp) IMPLIES PP?(sub_pos(fsp,p))
sub_pos_is_SPP: LEMMA
SPP?(s)(fsp) IMPLIES SPP?(s)(sub_pos(fsp,p))
Pos_Under_character: LEMMA
PP?(fsp1) & PP?(fsp2) & member_seq(p, Pos_Under(fsp1,fsp2))
IMPLIES EXISTS(j:below[fsp2`length]):
member_seq(p, sub_pos(fsp1,fsp2(j)))
union_positions: LEMMA
PP?(fsp1) & PP?(fsp2) IMPLIES
seq2set(fsp1) = seq2set(Pos_Over(fsp1, fsp2) o Pos_Equal(fsp1, fsp2) o Pos_Under(fsp1, fsp2))
%% Auxiliary lemma on sigma_rhs.
sigma_rhs_rest: LEMMA
fse`length = fss`length
IMPLIES rest(sigma_rhs(fss, fse)) = sigma_rhs(rest(fss), rest(fse))
%% Auxiliary lemma on sigma_rhs.
sigma_rhs_o: LEMMA
fse1`length = fss1`length AND fse2`length = fss2`length
IMPLIES
sigma_rhs(fss1 o fss2, fse1 o fse2) = sigma_rhs(fss1, fse1) o sigma_rhs(fss2, fse2)
%% Auxiliary lemma on subtermsOF.
subtermsOF_rest: LEMMA
SP?(t)(fsp) IMPLIES rest(subtermsOF(t,fsp)) = subtermsOF(t, rest(fsp))
% Lemma of inclusions of the rewriting relation in the parallel rewriting relation
% and the latter in the reflexive-transitive closure of the former relation.
parallel_reduction_inclusion: LEMMA
subset?(reduction?(E), parallel_reduction?(E))
& subset?(parallel_reduction?(E), RTC(reduction?(E)))
% The reflexive-transitive clousures of the rewriting and the parallel
% rewriting relations are equivalent.
parallel_reduction_RTC: LEMMA
RTC(reduction?(E)) = RTC(parallel_reduction?(E))
% Once you rewrite in parallel at positions fsp which are
% parallel to position p ("p || fsp"), a term in which position p is
% preserved is obtained.
replace_par_pos_preservs_pos: LEMMA
SPP?(t)(add_first(p,fsp)) AND fst`length = fsp`length
=> positionsOF(replace_par_pos(t, fsp, fst))(p)
% When you replace the subterms at the positions in fsp,
% those positions are preserved in the resulting term.
replace_par_pos_preservs_PP: LEMMA
SPP?(t)(fsp) AND fst`length = fsp`length
=> (FORALL (i : below[fsp`length]) : positionsOF(replace_par_pos(t, fsp, fst))(fsp(i)))
% Same of replace_par_pos_preserv_pos but instead for
% a unique position p || fsp for a sequence of positions fsq || fsp.
replace_par_pos_preservs_PP_o_PP: LEMMA
SPP?(t)(fsp o fsq ) AND fst`length = fsp`length
=> (FORALL (i : below[fsq`length]) : positionsOF(replace_par_pos(t, fsp, fst))(fsq(i)))
% If you replace the first parallel position firstly or lastly,
% that does not change the resulting term.
replace_par_pos_equivalence: LEMMA
SPP?(s)(fsp) AND fsp`length /= 0 AND fst`length = fsp`length
=> replace_par_pos(replaceTerm(s, fst(0), fsp(0)), rest(fsp), rest(fst)) =
replaceTerm(replace_par_pos(s, rest(fsp), rest(fst)), fst(0), fsp(0))
% Generalization of the previous result: you can pick up any position to start to work
% with replace_par_pos and that does not change the result.
replace_par_pos_equivalence1: LEMMA
SPP?(s)(fsp) AND fsp`length /= 0 AND fst`length = fsp`length AND n < fsp`length
=> replace_par_pos(replaceTerm(s, fst(n), fsp(n)), delete(fsp,n), delete[term](fst,n)) =
replace_par_pos(s,fsp,fst)
% If you apply replace_par_pos in positions fsp, then the subterm
% at any position p || fsp is preserved.
replace_par_pos_preservs_subterm: LEMMA
SPP?(t)(add_first(p,fsp)) AND fst`length = fsp`length
=> subtermOF(replace_par_pos(t, fsp, fst), p) = subtermOF(t, p)
% When one rewrites in parallel at fsp, the subterms of the resulting term
% at fsp are exatly the terms in fst.
replace_par_pos_subterm: LEMMA
SPP?(t)(fsp) AND fst`length = fsp`length
=> (FORALL (i : below[fsp`length]) : subtermOF(replace_par_pos(t, fsp, fst),fsp(i))=fst(i))
% If you replace the subterms at a composition of sequences 'fsp1 o fsp2',
% that are parallel, it is the same that doing it separately.
replace_par_pos_comp: LEMMA
SPP?(t)(fsp1 o fsp2) AND fst1`length = fsp1`length
AND fst2`length = fsp2`length
=> replace_par_pos(t, fsp1 o fsp2, fst1 o fst2) =
replace_par_pos(replace_par_pos(t, fsp1, fst1),fsp2, fst2)
%% In general, applying replace_par_pos at a parallel composition of sequences
%% fsp1 o fsp2 is commutative.
replace_par_pos_comp_commute: LEMMA
SPP?(t)(fsp1 o fsp2) AND fst1`length = fsp1`length AND fst2`length = fsp2`length
IMPLIES
replace_par_pos(t, fsp1 o fsp2, fst1 o fst2) =
replace_par_pos(t, fsp2 o fsp1, fst2 o fst1)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
complement_pos_set(p1,p): set[position] =
IF p1 <= p & p1 /= p
THEN {p2 | p=p1 o p2}
ELSE emptyset
ENDIF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
complement_pos(p,(fsp:PP)):
RECURSIVE finseq[position] =
IF length(fsp)=0 THEN empty_seq
ELSIF nonempty?(complement_pos_set(p,fsp`seq(0)))
THEN add_first(choose(complement_pos_set(p,fsp`seq(0))),
complement_pos(p,rest(fsp)))
ELSE complement_pos(p,rest(fsp))
ENDIF
MEASURE(length(fsp))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
parallel_pos_same_prefix: LEMMA
parallel(p1,p2) & p1= p o q1 & p2= p o q2
IMPLIES parallel(q1,q2)
complement_pos_character: LEMMA
PP?(fsp) & member_seq(p1, complement_pos(p,fsp))
IMPLIES EXISTS (i:below[fsp`length]):
fsp`seq(i)= p o p1
complement_pos_is_PP: LEMMA
PP?(fsp) IMPLIES PP?(complement_pos(p,fsp))
complement_pos_preservs_sub_pos_length1: LEMMA
PP?(fsp) IMPLIES
complement_pos(p, fsp)`length = sub_pos(fsp, p)`length
complement_pos_empty: LEMMA
PP?(add_first(p, fsp)) => complement_pos(p, fsp)`length = 0
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
comp_pos(p,fsp): finseq[position] = (# length := fsp`length,
seq := (LAMBDA (i: below[fsp`length]): p o fsp(i)) #);
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
comp_preservs_parallel_pos: LEMMA
parallel(p1,p2) IMPLIES parallel(p o p1,p o p2)
comp_preservs_parallel_pos2: LEMMA
parallel(p1,p2) IMPLIES parallel(p1 o q1,p2)
comp_preservs_parallel_pos3: LEMMA
parallel(p1,p2) IMPLIES parallel(p1 o q1,p2 o q2)
comp_pos_rest: LEMMA
comp_pos(p,rest(fsp)) = rest(comp_pos(p,fsp))
comp_pos_preservs_length: LEMMA
comp_pos(p, fsp)`length=fsp`length
comp_pos_character: LEMMA
FORALL(i:below[fsp`length]):
comp_pos(p,fsp)`seq(i)= p o fsp`seq(i)
comp_pos_is_PP: LEMMA
PP?(fsp) IMPLIES PP?(comp_pos(p,fsp))
%% Replacing at the position q of t by the result of replacing in parallel at positions fsp of s
%% gives as result the same as replacing at positions q o fsp of t[q<-s].
replace_replace_par_pos: LEMMA
positionsOF(t)(q) AND SPP?(s)(fsp) AND fst`length = fsp`length
IMPLIES
replaceTerm(t, replace_par_pos(s,fsp,fst), q) = replace_par_pos(replaceTerm(t,s,q), comp_pos(q,fsp), fst)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
complement_pos_preservs_sub_pos_length: LEMMA
PP?(fsp) IMPLIES
complement_pos(p1,complement_pos(p, fsp))`length
= sub_pos(fsp, p o p1)`length
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Pos_Over_character: LEMMA
PP?(fsp1) & PP?(fsp2)
=> FORALL (i:below[Pos_Over(fsp1,fsp2)`length]):
PP?(add_first(Pos_Over(fsp1,fsp2)`seq(i),fsp2))
OR EXISTS (j:below[fsp2`length]):
Pos_Over(fsp1,fsp2)`seq(i) <= fsp2`seq(j)
& Pos_Over(fsp1,fsp2)`seq(i) /= fsp2`seq(j)
Pos_Equal_character: LEMMA
PP?(fsp1) & PP?(fsp2)
=> FORALL (i:below[Pos_Equal(fsp1,fsp2)`length]):
EXISTS (j:below[fsp2`length]):
Pos_Equal(fsp1,fsp2)`seq(i) = fsp2`seq(j)
Pos_Equal_is_PP: LEMMA
PP?(fsp1) & PP?(fsp2)
=> PP?(Pos_Equal(fsp1, fsp2))
Pos_Over_and_Pos_Equal_is_PP: LEMMA
PP?(fsp1) & PP?(fsp2)
=> PP?(Pos_Over(fsp1, fsp2) o Pos_Over(fsp2, fsp1) o Pos_Equal(fsp1,fsp2))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
comp_pos_in_SP_preservs_SP_in_replace: LEMMA
SPP?(t)(fsp) & SP?(s)(fsp1) & fsp`length > 0 IMPLIES
SP?(replaceTerm(t, s, fsp`seq(0)))(comp_pos(fsp`seq(0), fsp1) o rest(fsp))
comp_pos_in_PP_preservs_PP: LEMMA
PP?(fsp) & PP?(fsp1) & fsp`length > 0 IMPLIES
PP?(comp_pos(fsp`seq(0), fsp1) o rest(fsp))
comp_pos_in_SPP_preservs_SPP_in_replace: LEMMA
SPP?(t)(fsp) & SPP?(s)(fsp1) & fsp`length > 0 IMPLIES
SPP?(replaceTerm(t, s, fsp`seq(0)))(comp_pos(fsp`seq(0), fsp1) o rest(fsp))
comp_pos_in_SPP_preservs_SPP_in_replace_par_pos: LEMMA
SPP?(t)(fsp) & fsp`length=fst`length & fsp`length /= 0 &
SPP?(fst`seq(0))(fsp1) &
SPP?(replace_par_pos(t, fsp, fst))(fsp2) &
PP?(add_first(fsp`seq(0),fsp2)) IMPLIES
SPP?(replace_par_pos(t, fsp, fst))(comp_pos(fsp`seq(0), fsp1) o fsp2)
parallel_reduction_reflexive: LEMMA reflexive?(parallel_reduction?(E))
non_ambiguous_implies_same_term: LEMMA
NOT Ambiguous?(E) & positionsOF(s)(p) &
reduction_fix?(E)(s,t1,p) &
reduction_fix?(E)(s,t2,p)
IMPLIES t1 = t2
parallel_reduction_context_aux2: LEMMA
SPP?(t)(fsp) AND fst1`length = fsp`length AND fst2`length = fsp`length AND
(FORALL (i : below[fsp`length]): parallel_reduction?(E)(fst1(i),fst2(i)))
IMPLIES EXISTS (fsq:SPP(replace_par_pos(t, fsp, fst1))):
parallel_reduction_fix?(E)(replace_par_pos(t, fsp, fst1),replace_par_pos(t, fsp, fst2), fsq)
AND (FORALL(p:positions?(t)): PP?(add_first(p,fsp)) => PP?(add_first(p,fsq)))
parallel_reduction_context: LEMMA
SPP?(t)(fsp) AND fst1`length = fsp`length AND fst2`length = fsp`length AND
(FORALL (i : below[fsp`length]): parallel_reduction?(E)(fst1(i),fst2(i)))
IMPLIES
parallel_reduction?(E)(replace_par_pos(t, fsp, fst1),replace_par_pos(t, fsp, fst2))
replace_par_pos_of_app_is_app: LEMMA
app?(t) & SPP?(t)(fsp) & fst`length = fsp`length IMPLIES
fsp = #(empty_seq) OR
app?(replace_par_pos(t, fsp, fst))
replace_par_pos_preservs_f: LEMMA
app?(t) & SPP?(t)(fsp) & fst`length = fsp`length IMPLIES
fsp = #(empty_seq) OR
f(t) = f(replace_par_pos(t,fsp,fst))
parallel_reduction_closed_subs: LEMMA
(FORALL (x: Vars?(t)): parallel_reduction?(E)(ext(sigma)(x), ext(theta)(x)))
IMPLIES
parallel_reduction?(E)(ext(sigma)(t), ext(theta)(t))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
compo_sufix(fsp:PP, p):
finseq[position] = (# length := fsp`length,
seq := (LAMBDA(i:below[fsp`length]): fsp`seq(i) o p) #)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
parallel_reduction_result: LEMMA
Orthogonal?(E) & E(e) & SPP?(ext(sigma)(lhs(e)))(fsp) &
parallel_reduction_fix?(E)(ext(sigma)(lhs(e)), t, fsp)
IMPLIES
fsp = #(empty_seq) OR
EXISTS(theta): t = ext(theta)(lhs(e))
replace_par_pos_subterm2: LEMMA
SPP?(s)(fsp) & member_seq(p1, fsp) &
p <= p1 & p /= p1 &
fsp`length = fst`length IMPLIES
EXISTS fst1 : (complement_pos(p, fsp)`length = fst1`length &
subtermOF(replace_par_pos(s, fsp, fst), p) =
replace_par_pos(subtermOF(s, p), complement_pos(p, fsp), fst1))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
C(e, sigma, s, t, (p|positionsOF(s)(p) & positionsOF(t)(p))): bool =
subtermOF(s, p) = ext(sigma)(lhs(e)) AND
subtermOF(t, p) = ext(sigma)(rhs(e))
D(s, t, (fsp|SPP?(s)(fsp) & SPP?(t)(fsp)), E)(i:below[fsp`length], e): bool =
member(e, E) &
EXISTS sigma : C(e, sigma, s, t, fsp`seq(i))
G(s, t, (fsp|SPP?(s)(fsp) & SPP?(t)(fsp)),E)(i:below[fsp`length], sigma): bool =
EXISTS (e|member(e, E)) : C(e, sigma, s, t, fsp`seq(i))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
parallel_reduction_variables: LEMMA
NOT Ambiguous?(E) & E(e) &
SPP?(ext(sigma)(lhs(e)))(fsp) &
parallel_reduction_fix?(E)(ext(sigma)(lhs(e)), ext(theta)(lhs(e)),fsp) &
NOT fsp = #(empty_seq)
IMPLIES
FORALL (x:Vars?(lhs(e))):
parallel_reduction?(E)(ext(sigma)(x), ext(theta)(x))
Parallel_Moves_Lemma: LEMMA
Orthogonal?(E) & member(e,E) &
parallel_reduction?(E)(ext(sigma)(lhs(e)), t)
IMPLIES EXISTS s: parallel_reduction?(E)(ext(sigma)(rhs(e)),s) &
parallel_reduction?(E)(t,s)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
replace_par_pos_dominance: LEMMA
SPP?(t)(fsp) & SPP?(t)(fsp1) & parallel_reduction_fix?(E)(t,s,fsp1) &
(FORALL(i:below[fsp1`length]):
EXISTS(j:below[fsp`length]):fsp`seq(j) <= fsp1`seq(i))
IMPLIES s = replace_par_pos(t,fsp,subtermsOF(s,fsp))
Pos_Over_and_Pos_Equal_dominance: LEMMA
SPP?(t)(fsp1) & SPP?(t)(fsp2) IMPLIES
(FORALL(i:below[fsp1`length]):
EXISTS(j:below[(Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2))`length]):
(Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2))`seq(j) <= fsp1`seq(i))
divergence_in_Pos_Over_aux: LEMMA
SPP?(t)(fsp2) &
parallel_reduction_fix?(E)(t, t2, fsp2) &
positionsOF(t)(p) &
member_seq(p, Pos_Over( #(p), fsp2))
=> parallel_reduction_fix?(E)(subtermOF(t, p), subtermOF(t2, p), complement_pos(p, fsp2))
divergence_in_Pos_Over: LEMMA
SPP?(t)(fsp1) & SPP?(t)(fsp2) &
parallel_reduction_fix?(E)(t, t1, fsp1) &
parallel_reduction_fix?(E)(t, t2, fsp2) &
member_seq(p, Pos_Over(fsp1, fsp2))
=> (EXISTS((e | member(e, E)), sigma):
subtermOF(t, p) = ext(sigma)(lhs(e)) &
subtermOF(t1, p) = ext(sigma)(rhs(e)) &
parallel_reduction?(E)(subtermOF(t, p),subtermOF(t2,p)) )
subterm_joinability: LEMMA
Orthogonal?(E) &
SPP?(t)(fsp1) & SPP?(t)(fsp2) &
parallel_reduction_fix?(E)(t,t1,fsp1) &
parallel_reduction_fix?(E)(t,t2,fsp2) &
fsp = Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2)
IMPLIES FORALL(i:below[fsp`length]):
EXISTS s :
parallel_reduction?(E)(subtermOF(t1,fsp(i)), s) &
parallel_reduction?(E)(subtermOF(t2,fsp(i)), s)
subterms_joinability: LEMMA
Orthogonal?(E) &
SPP?(t)(fsp1) & SPP?(t)(fsp2) &
parallel_reduction_fix?(E)(t,t1,fsp1) &
parallel_reduction_fix?(E)(t,t2,fsp2) &
fsp = Pos_Over(fsp1,fsp2) o Pos_Over(fsp2,fsp1) o Pos_Equal(fsp1,fsp2)
IMPLIES EXISTS fst : fsp`length = fst`length AND
FORALL(i:below[fsp`length]):
parallel_reduction?(E)(subtermOF(t1,fsp(i)), fst(i)) &
parallel_reduction?(E)(subtermOF(t2,fsp(i)), fst(i))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
parallel_reduction_has_DP: LEMMA
Orthogonal?(E) => diamond_property?(parallel_reduction?(E))
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Orthogonal_implies_confluent: LEMMA
FORALL (E : Orthogonal) :
LET RRE = reduction?(E) IN
confluent?(RRE)
END orthogonality
[ Dauer der Verarbeitung: 0.36 Sekunden
(vorverarbeitet)
]
|
