|
%%-------------------** Abstract Reduction System (ARS) **-------------------
%%
%% Authors : Ana Cristina Rocha Oliveira
%% Mauricio Ayala Rincon
%% Universidade de Brasília - Brasil
%%
%% and
%%
%% Andre Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% Last Modified On: October 15, 2008
%%
%%---------------------------------------------------------------------------
%%%% This theory contains some results and exercises from the book TeReSe %%%
confluence_commute[T: TYPE] : THEORY
BEGIN
IMPORTING noetherian[T],
results_confluence[T]
R, R1, R2, R3 : VAR PRED[[T, T]]
x, y, z, r, s : VAR T
% Terminology
semi_commute?(R1,R2): bool =
FORALL x, y, z: R1(x,y) & RTC(R2)(x,z) =>
EXISTS r: RTC(R2)(y,r) & RTC(R1)(z,r)
sub_commutative?(R): bool =
FORALL x, y, z: R(x,y) & R(x,z) =>
EXISTS r: RC(R)(y,r) & RC(R)(z,r)
request?(R1,R2): bool =
FORALL x, y, z: RTC(R1)(x,y) & RTC(R2)(x,z) =>
EXISTS r, s: RTC(R2)(y,r) & RTC(R1)(z,s) & RTC(R2)(s,r)
refinement?(R1,R2): bool =
FORALL x, y: R1(x,y) => RTC(R2)(x,y)
ref_compatible?(R1,R2): bool =
refinement?(R1,R2) & (FORALL x, y: RTC(R2)(x,y) => joinable?(R1)(x,y))
postponement?(R1,R2): bool =
FORALL x, y: LET R = union(R1,R2) IN RTC(R)(x,y) =>
EXISTS z: RTC(R1)(x,z) & RTC(R2)(z,y)
UN_terese?(R): bool = FORALL x, y :( is_normal_form?(R)(x) &
is_normal_form?(R)(y) &
EC(R)(x,y) ) =>
x = y
UNseta_terese?(R): bool = FORALL x, y :( is_normal_form?(R)(x) &
is_normal_form?(R)(y) &
(EXISTS z : RTC(R)(z,x) & RTC(R)(z,y)) )
=>
x = y
% Auxiliary Lemmas
RC_RTC_is_RTC : LEMMA RC(RTC(R)) = RTC(R)
RTC_o_RTC_is_RTC : LEMMA RTC(R)(x,y) & RTC(R)(y,z) => RTC(R)(x,z)
RC_o_RTC_is_RTC : LEMMA RC(R)(x,y) & RTC(R)(y,z) => RTC(R)(x,z)
RTC_converse_RTC_R: LEMMA RTC(R)(x,y) <=> RTC(converse(R))(y,x)
% Exercice: 1.3.6 [Staples 1975], terese
semi_comm_implies_comm: LEMMA semi_commute?(R1,R2) => commute?(R1,R2)
% Proposition: 1.1.10, terese
sub_comm_rtc_implies_conf : LEMMA sub_commutative?(RTC(R)) => confluent?(R)
% Exercice: 1.3.8 (i), terese
conf_local_request_implies_request : LEMMA
confluent?(R2) & (FORALL x, y, z: RTC(R1)(x,y) & R2(x,z) =>
EXISTS r, s: RTC(R2)(y,r) & RTC(R1)(z,s) & RTC(R2)(s,r) )
=> request?(R1,R2)
% Exercice: 1.3.8 (ii), terese
comp_rtc_req_conf_impl_diamond: LEMMA
LET R3 = RTC(R1) o RTC(R2) IN
((request?(R1,R2) & confluent?(R2) &
(FORALL x, y, z: RTC(R1)(x,y) & RTC(R1)(x,z) => EXISTS r: R3(y,r) & R3(z,r)))
=>
diamond_property?(R3) )
union_req_conf_is_confluent : LEMMA
request?(R1,R2) & confluent?(R2) & (LET R3 = RTC(R1) o RTC(R2) IN
(FORALL x, y, z: RTC(R1)(x,y) & RTC(R1)(x,z) => EXISTS r: R3(y,r) & R3(z,r)))
=>
(LET R = union(R1, R2) IN
(confluent?(R)))
% Exercice: 1.3.8 (iii), terese
comp_rtc_confs_req_impl_diamond: LEMMA
confluent?(R1) & confluent?(R2) & request?(R1,R2)
=> (LET R3 = RTC(R1) o RTC(R2) IN diamond_property?(R3))
union_confs_req_is_confluent: LEMMA
confluent?(R1) & confluent?(R2) & request?(R1,R2)
=> (LET R = union(R1, R2) IN (confluent?(R)))
% Exercice: 1.3.5 (i), terese
CR_iff_PP: LEMMA
church_rosser?(R) <=> postponement?(R,converse(R))
confluent_iff_postponement: LEMMA
confluent?(R) <=> postponement?(R,converse(R))
% Exercice: 1.3.5 (ii), terese
% 1.3.5. Exercise [Hindley 1964]
hip_Hindley_implies_semi_comm : LEMMA
(FORALL x, y, z : (R1(x, y) & R2(x, z) => EXISTS r : R2(y, r) & RC(R1)(z, r)))
IMPLIES semi_commute?(R1, R2)
lemma_Hindley_1964 : LEMMA
(FORALL x, y, z: (R1(x, y) & R2(x, z) => EXISTS r : R2(y, r) & RC(R1)(z, r)))
IMPLIES commute?(R1, R2)
% Exercice: 1.3.9 (i), terese
ref_condition_to_refcomp : LEMMA
refinement?(R1,R2) => (ref_compatible?(R1,R2)
<=>
(FORALL x, y:(R2 o RTC(R1))(x,y) => joinable?(R1)(x,y)))
% Auxiliar for Rosen 73' Lemma
semi_implies_CR: LEMMA semi_confluent?(R) => church_rosser?(R)
semi_implies_conf: LEMMA semi_confluent?(R) => confluent?(R)
sub_comm_implies_semi_conf : LEMMA sub_commutative?(R) => semi_confluent?(R)
sub_comm_implies_conf : LEMMA sub_commutative?(R) => confluent?(R)
% Exercice: 1.3.3 [Rosen 1973]
lemma_Rosen_1973 : LEMMA
RTC(R1) = RTC(R2) & sub_commutative?(R1) =>
confluent?(R2)
% Exercice: 1.3.2
lcomm_and_snunion_implies_comm : LEMMA locally_commute?(R1,R2) &
noetherian?(union(R1,R2))
=>
commute?(R1,R2)
% Exercice: 1.3.10
UN_implies_UNseta : LEMMA UN_terese?(R) => UNseta_terese?(R)
END confluence_commute
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
