Quelle fixpoints.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Definition and properties of Fixpoints
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% Note carefully:
%
% FIX(f)   is the set of all fixpoints of any function.
% fix(phi) is the least fixpoint of an increasing (ie monotonic) function.
%
%   And especially: only when the function (psi) is continuous do we have
%
% psi(fix(psi)) = fix(psi)
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

fixpoints[T:TYPE+, (IMPORTING orders@directed_orders[T])
          <=:(pointed_directed_complete_partial_order?[T])]: THEORY

BEGIN

  IMPORTING fun_preds_partial[T,T,<=,<=],
            orders@directed_order_props[T,<=]

  n:   VAR nat
  x,y: VAR T
  f,g: VAR [T -> T]
  phi: VAR (increasing?)
  X:   VAR (nonempty?[T])
  D:   VAR directed

  unique_bottom: LEMMA least?(fullset[T],<=)(x) AND
                       least?(fullset[T],<=)(y) IMPLIES x = y

  bottom: (least?(fullset[T],<=))

  bottom_le:  LEMMA bottom <= x
  le_bottom:  LEMMA (x <= bottom) IMPLIES x = bottom
  nonempty_T: LEMMA nonempty?(fullset[T])

  IMPORTING algebra@monoid[[T->T],function_props[T,T,T].o,(LAMBDA x: x)],
            scott[T,<=],
            orders@chain[T,<=],
            fun_preds_partial[nat,T,reals.<=,<=]

  FIX_APPROX(phi):set[T] = image((LAMBDA n: power(phi,n)(bottom)),fullset[nat])
  FIX(f)         :set[T] = {x | f(x) = x}

  lub_add_bottom:       LEMMA lub(D) = lub(add(bottom,D))
  increasing_phi_n:     LEMMA increasing?(power(phi,n))
  increasing_power:     LEMMA increasing?(LAMBDA n: power(phi,n)(bottom))
  fix_approx_nonempty:  LEMMA nonempty?(FIX_APPROX(phi))
  fix_approx_chain:     LEMMA chain?(FIX_APPROX(phi))
  ne_chain_is_directed: LEMMA chain?(X) IMPLIES directed?(<=)(X)
  lub_emptyset:         LEMMA lub(emptyset[T]) = bottom

  fix(phi):T = lub(FIX_APPROX(phi))

  member_FIX:           LEMMA member(x,FIX(f)) IMPLIES f(x) = x
  fix_is_least:         LEMMA member(x,FIX(phi)) IMPLIES fix(phi) <= x
  fix_le:               LEMMA fix(phi) <= phi(fix(phi))

  IMPORTING scott_continuity[T,T,<=,<=]

  psi: VAR (continuous?)

  fix_in_FIX:           LEMMA member(fix(psi),FIX(psi))
  nonempty_FIX:         LEMMA nonempty?(FIX(psi))
  fix_prop:             LEMMA psi(fix(psi)) = fix(psi)
  fixpoint_contraction: LEMMA psi(x) <= x => fix(psi) <= x

END fixpoints

quality87%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.