|
%%-------------------** Abstract Reduction System (ARS) **-------------------
%%
%% Authors : Andre Luiz Galdino
%% Universidade Federal de Goiás - Brasil
%%
%% and
%%
%% Mauricio Ayala Rincon
%% Universidade de Brasília - Brasil
%%
%% Last Modified On: December 02, 2006
%%
%%---------------------------------------------------------------------------
results_confluence[T : TYPE] : THEORY
BEGIN
IMPORTING ars_terminology[T]
R, R1, R2 : VAR PRED[[T, T]]
x, y, z, r : VAR T
%%---------------------** Basic Results: Confluence **------------------------
%%
%%
%% - reduct_transitive: If x -> y and y and z are joinable then
%% x and z are joinable.
%%
%%
%% - semi_and_iterate: If -> is semi-confluent and x <->* y (see definition
%% of <->* in the file relations_closure) then x and y
%% are joinable.
%%
%%
%% - Confl_implies_Semi, Semi_implies_CR, and CR_implies_Confl: Show that
%%
%% -> is CR iff -> is confluent iff -> is semi-confluent.
%%
%%
%% - strong_and_iterate: If -> is strongly confluent and y <- x ->* z then
%% exists r such that y ->* r =<- z.
%%
%% In other words,
%%
%% i) strongly confluent implies semi-confluent: Str_Confl_implies_Semi_Confl.
%%
%% ii) strongly confluent implies confluent: Strong_Confl_implies_Confl.
%%
%%
%% - DP_implies_StC: If -> has the diamond property then -> is strongly
%% confluent.
%%
%%
%% - R1_Confl_implies_R2_Confl: If ->* = -->* then -> is confluent iff
%% --> is confluent.
%%
%%
%% - R1_equal_R2: If -> contained in -->, and --> contained in ->* then
%% ->* = -->*.
%%
%%
%% - R2_Str_Confl_implies_R1_Confl: If -> contained in -->, and -->
%% contained in ->* and --> is strongly
%% confluent then -> is confluent.
%%
%%
%% - Confluence_Commute: If -> and --> are confluent and commute, then
%% ->* o -->* has the diamond property.
%%
%%
%% - R1_R2_RTC_R1_R2: For arbitrary -> and --> we have
%% (-> union -->) contained in (->* o -->*) and
%% (->* o -->*) contained in (-> union -->)*.
%%
%%
%% - Commutative_Union_Lemma: This lemma tells us that in certain cases union
%% preserves confluence. In other words,
%% If -> and --> are confluent and commute, then
%% -> o --> is also confluent.
%%
%%
%%---------------------------------------------------------------------------
Joinable_implies_Equiv: LEMMA joinable?(R)(x,y) => EC(R)(x,y)
reduct_transitive: LEMMA R(x,y) & joinable?(R)(y,z) => joinable?(R)(x,z)
semi_and_iterate: LEMMA FORALL (n: nat): semi_confluent?(R) &
iterate(SC(R), n)(x,y) =>
joinable?(R)(x,y)
Confl_implies_Semi: THEOREM confluent?(R) => semi_confluent?(R)
Semi_implies_CR: THEOREM semi_confluent?(R) => church_rosser?(R)
CR_iff_Confluent: THEOREM church_rosser?(R) <=> confluent?(R)
strong_and_iterate: LEMMA FORALL (n: nat): strong_confluent?(R) & R(x,y)
& iterate(R, n)(x, z) =>
EXISTS r: RTC(R)(y,r) & RC(R)(z, r)
Str_Confl_implies_Semi_Confl: THEOREM strong_confluent?(R)
=> semi_confluent?(R)
Strong_Confl_implies_Confl: COROLLARY strong_confluent?(R) => confluent?(R)
DP_implies_StC: LEMMA diamond_property?(R) => strong_confluent?(R)
R1_Confl_iff_R2_Confl: LEMMA RTC(R1) = RTC(R2) =>
( confluent?(R1) <=> confluent?(R2) )
R1_equal_R2: LEMMA subset?(R1,R2) & subset?(R2,RTC(R1)) => RTC(R1) = RTC(R2)
R2_Str_Confl_implies_R1_Confl: COROLLARY subset?(R1, R2)
& subset?(R2, RTC(R1))
& strong_confluent?(R2) => confluent?(R1)
Confluence_Commute: THEOREM confluent?(R1) & confluent?(R2) & commute?(R1,R2)
=> diamond_property?(RTC(R1) o RTC(R2))
R1_R2_RTC_R1_R2: LEMMA subset?(union(R1, R2), RTC(R1) o RTC(R2)) &
subset?(RTC(R1) o RTC(R2), RTC(union(R1, R2)))
Commutative_Union_Lemma: THEOREM confluent?(R1) & confluent?(R2) &
commute?(R1,R2) => confluent?(union(R1, R2))
end results_confluence
¤ Dauer der Verarbeitung: 0.16 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.
|
