Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
div.prf
Sprache: Unknown
|
%%-------------------** 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
%%
%%---------------------------------------------------------------------------
noetherian[T : TYPE] : THEORY
BEGIN
IMPORTING ars_terminology[T],
orders@well_foundedness[T]
P : VAR PRED[T]
R : VAR PRED[[T, T]]
x, y : VAR T
%%------------------------** Termination (Noetherian) **--------------------
%%
%% A reduction -> (relation R) is
%%
%% - noetherian (terminating) iff there is no infinite
%% descending chain a0 -> a1 -> .... In other words, a relation -> is
%% noetherian if the inverse (converse) relation of -> is well founded.
%%
%% - convergent if is confluent and noetherian.
%%
%% - R_is_Noet_iff_TC_is: ->+ is terminating iff -> is.
%%
%%
%% - noetherian_induction: To prove P(x) for all x, it suffices to prove P(x)
%% under the assunption that P(y) holds for all
%% successors y of x.
%%
%%--------------------------------------------------------------------------
noetherian?(R): bool = well_founded?(converse(R))
noetherian: TYPE = (noetherian?)
convergent?(R): bool = confluent?(R) & noetherian?(R)
R_is_Noet_iff_TC_is: LEMMA noetherian?(R) <=> noetherian?(TC(R))
noetherian_induction: LEMMA
(FORALL (R: noetherian, P):
(FORALL x:
(FORALL y: TC(R)(x, y) IMPLIES P(y))
IMPLIES P(x))
IMPLIES
(FORALL x: P(x)))
END noetherian
[ zur Elbe Produktseite wechseln0.4Quellennavigators
Analyse erneut starten
]
|
|
