Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/TRS/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 5 kB

SSL confluence_commute.pvs Interaktion und
PortierbarkeitPVS

%%-------------------** 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

quality59%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.11Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.