|
%%-------------------** 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_normal_form[T : TYPE] : THEORY
BEGIN
IMPORTING results_confluence[T],
noetherian[T]
R : VAR PRED[[T, T]]
x, y, u, v : VAR T
%%--------------------** Basic Results: Normal Form **------------------------
%%
%%
%% - NF_doesnot_rewrite: If x is in normal form and x ->* y then x = y.
%%
%%
%%%% If -> is confluent and x <->* y then
%%
%% - NF_implies_RTC: x ->* y if y is in normal form,
%%
%% - NFs_implies_Equal: x = y if both x and y are in normal form.
%%
%%
%% - Norm_and_Confl_implies_UNF_NF: If -> is normalizing and confluent,
%% every element has a unique normal form.
%%
%%
%%%% If x has a unique normal form, the latter is denoted by x|
%%
%% - Normalizing_and_Confl: If -> is normalizing and confluent then x <->* y
%% iff x| = y|.
%%
%%
%% - Normal_Confl_iff_UNF: -> is normalizing and confluent iff
%% every element has a unique normal form.
%%
%%
%% - Noetherian_implies_normalizing: Any terminating relation is normalizing.
%%
%%
%% - Convergent_UF: If -> is convergent, then every element has a unique
%% normal form.
%%
%%
%% - Noet_and_Confl_iff_UNF: If -> is terminating, then -> is confluent iff
%% every element has a unique normal form.
%%
%%
%% - Convergent_iff_eqNF: If -> is convergent, then x <->* y iff x| = y|.
%%
%%
%%---------------------------------------------------------------------------
NF_doesnot_rewrite: LEMMA ( is_normal_form?(R)(x) & RTC(R)(x,y) => x = y )
NF_implies_RTC: LEMMA ( confluent?(R) & EC(R)(x,y) ) =>
(is_normal_form?(R)(y) => RTC(R)(x,y) )
NFs_implies_Equal: LEMMA ( confluent?(R) & EC(R)(x,y) ) =>
(is_normal_form?(R)(x) & is_normal_form?(R)(y)
=> x = y )
Norm_and_Confl_implies_UNF: LEMMA normalizing?(R) & confluent?(R) =>
FORALL x: has_unique_nf?(R,x)
Normalizing_and_Confl: LEMMA ( normalizing?(R) & confluent?(R) ) =>
EXISTS u, v: unique_nf?(R)(x,u) & unique_nf?(R)(y,v)
& EC(R)(x,y) <=> u = v
Normal_Confl_iff_UNF: LEMMA normalizing?(R) & confluent?(R) <=>
FORALL x: has_unique_nf?(R,x)
Noetherian_implies_normalizing: LEMMA noetherian?(R) => normalizing?(R)
Convergent_UNF: LEMMA convergent?(R) => FORALL x: has_unique_nf?(R,x)
Noet_and_Confl_iff_UNF: LEMMA noetherian?(R) =>
( confluent?(R) <=>
FORALL x: has_unique_nf?(R,x) )
Convergent_iff_eqNF: LEMMA convergent?(R) =>
( EC(R)(x,y) <=>
(FORALL u,v: normal_form?(R)(x,u)
& normal_form?(R)(y,v)
=> u = v) )
end results_normal_form
¤ Dauer der Verarbeitung: 0.23 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.
|
