|
%%-------------------** 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: October 15, 2008
%%
%%---------------------------------------------------------------------------
modulo_equivalence[T : TYPE] : THEORY
BEGIN
IMPORTING noetherian[T]
R, S : VAR PRED[[T, T]]
Eq : VAR equivalence
x, y,
z, w,
u, v : VAR T
R_Eq(R, Eq) : PRED[[T, T]] = Eq o R o Eq
SC_Eq(R, Eq) : PRED[[T, T]] = union(SC(R), Eq)
Eq_Eq(R, Eq) : equivalence = EC(SC_Eq(R, Eq))
joinable_m?(R, Eq)(x,y) : bool = EXISTS u,v: RTC(R)(x,u) &
Eq(u,v) & RTC(R)(y,v)
church_rosser_m?(R, Eq) : bool = FORALL x, y: Eq_Eq(R, Eq)(x,y) =>
joinable_m?(R, Eq)(x,y)
local_confluent_m?(R, Eq) : bool = FORALL x, y, z: R(x,y) & R(x,z) =>
joinable_m?(R, Eq)(y,z)
confluent_m?(R, Eq) : bool = FORALL x, y, z, w: RTC(R)(x,z) &
Eq(x,y) &
RTC(R)(y,w) =>
joinable_m?(R, Eq)(z,w)
has_unique_nf_m?(R, Eq) : bool = FORALL x, y, u, v: is_normal_form?(R)(u) &
is_normal_form?(R)(v) &
RTC(R)(x,u) &
Eq_Eq(R, Eq)(x,y) &
RTC(R)(y,v) => Eq(u,v)
locally_coherent?(R, Eq, S) : bool = symmetric?(S) &
FORALL x, y, z: R(x,y) &
S(x,z) => joinable_m?(R, Eq)(y,z)
noetherian_m?(R, Eq) : bool = well_founded?(converse(R o Eq))
%%--------------------------------------
van_oostrom94 : LEMMA diamond_property?(RTC(R) o Eq) => confluent_m?(R, Eq)
newman_lemma_general : THEOREM noetherian?(R) =>
(local_confluent_m?(R, Eq) &
locally_coherent?(R, Eq, Eq) <=>
confluent_m?(R, Eq))
END modulo_equivalence
[ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
]
|
