Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sqrtx.prf Sprache: PVS

Original von: PVS^©

%------------------------------------------------------------------------------
% Continuous Functions bewteen Scott Topologies
%
% All references are to BA Davey and HA Priestly "Introduction to Lattices and
% Orders", CUP, 1990
%
% We give the Domain Theoretical formulation of Continuity
% (scott_continuous_def) and show that the pointwise order on functions is
% itself directed complete (pointwise_complete).
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

scott_continuity[T1,T2:TYPE, (IMPORTING orders@directed_orders)
                 le1:(directed_complete_partial_order?[T1]),
                 le2:(directed_complete_partial_order?[T2])]: THEORY

BEGIN

  IMPORTING scott[T1,le1], scott[T2,le2], fun_preds_partial[T1,T2,le1,le2],
            topology@continuity_def[T1,scott_open_sets[T1,le1],
                                    T2,scott_open_sets[T2,le2]],
            topology@continuity[T1,scott_open_sets[T1,le1],
                                T2,scott_open_sets[T2,le2]]

  D: VAR directed[T1,le1]
  a: VAR T2
  f: VAR [T1->T2]
  g: VAR (increasing?)

% The following three Lemmata are D&P 3.15 (i)

  lub_set_image:  LEMMA lub_set?(image(g,D))
  directed_image: LEMMA directed?[T2,le2](image(g,D))
  lub_image:      LEMMA le2(lub(image(g,D)),g(lub(D)))

% The following is D&P 3.15 (ii)

  lub_image_increasing: LEMMA
       (FORALL D: directed?[T2,le2](image(f,D)) AND
                  le2(lub[T2,le2](image(f,D)),f(lub[T1,le1](D))))
       IMPLIES increasing?(f)

  lub_preserving?(f):bool = FORALL D: lub_set?(image(f,D)) IMPLIES
                                        f(lub(D)) = lub(image(f,D))

  scott_continuous?(f):bool = increasing?(f) AND lub_preserving?(f)

  scott_continuous: TYPE = (scott_continuous?)

  scott_continuous_def: LEMMA continuous?(f) IFF scott_continuous?(f)

  scott_continuous_is_continuous:
                   JUDGEMENT (scott_continuous?) SUBTYPE_OF (continuous?)
  continuous_is_scott_continuous:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (scott_continuous?)
  continuous_is_increasing:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (increasing?)
  continuous_is_lub_preserving:
                   JUDGEMENT (continuous?)       SUBTYPE_OF (lub_preserving?)

  IMPORTING structures@const_fun_def[T1,T2],
            topology@constant_continuity[T1,scott_open_sets[T1,le1],
                                         T2,scott_open_sets[T2,le2]]

  const_scott_continuous: JUDGEMENT const_fun(a) HAS_TYPE scott_continuous

  IMPORTING orders@directed_orders[(scott_continuous?)],
            orders@pointwise_orders[T1,T2]

  pointwise_complete: LEMMA
    directed_complete?[(scott_continuous?)](pointwise(le2))

  scott_continuous_dcpo: LEMMA
    directed_complete_partial_order?[(scott_continuous?)](pointwise(le2))

  IMPORTING scott[(scott_continuous?),(pointwise(le2))]

END scott_continuity

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.