Quellcode-Bibliothek linear_map.pvs Interaktion und
PortierbarkeitPVS

% --------------------------------------------------------------
% Linear Algebra library
% Heber Herencia-Zapana NIA
% Gilberto Pérez        University of Coruña Spain
% Pablo Ascariz         University of Coruña Spain
% Felicidad Aguado      University of Coruña Spain
% Date: December, 2013
% ----------------------------------------------------------------
%   This theory defines the map operator.
%
% --------------------------------------------------------------
%  This file is a single component of a library of linear
%  algebra theories.
%  --------------------------------------------------------------
%  For the most part, we follow the treatmet in the following texts
%
% [FIS] Linear Algebra, S. Friedburg, A.  Insel, and L. Spense, 3rd edition, Prentice-Hall.
%
% [SA]  Linear Algebra Done Right,  S. Axler. 2nd Edition. Springer-Verlag.
%
%   [D]  Topology,  J. Dungundji, Allen and Bacon Co.
%
%   [K]  Introductory Functional Analysis,  Kreysizg, Wiley.
%
%   [R]  Convex Analysis, R. Rockafellar, Princeton University Press.
%
%   [J]   A Lecture or the S-Procedure, U. Jonsson.
%
%
%
%-------------------------------------------------------------

linear_map: theory

BEGIN

IMPORTING vectors@vectors

n,m :VAR posnat

%------------------------------------------------------------------------
% A map from an n dimensional vector space to an m dimensional vector
% space takes a n-dimensional vector to an m-dimensional vector.
% It is defined as a record given by: the dimension of the domain, the
% dimension of the codomain, and the function from the domain to the
% codomain
%------------------------------------------------------------------------

Maping: TYPE = [#dom: posnat,codom: posnat,mp: [Vector[dom]->Vector[codom]]#]

Map(n,m): TYPE = {f: Maping | f`dom = n and f`codom = m}

%-----------------------------------------------------------------------------
% Next we define operations with mappings.
% same_dim? and same? provide the restrictions relating to the domain and
% codomain which allow us to define the sum and the composition, respectively
%-----------------------------------------------------------------------------

same_dim?(f: Maping)(g: Maping):bool = f`dom = g`dom and f`codom = g`codom;

same?(f: Maping)(g: Maping): bool = f`dom = g`codom;

+(f: Maping,(g: (same_dim?(f)))): Maping = f WITH [`mp:= lambda(x: Vector[f`dom]): f`mp(x) + g`mp(x)];

*(a: real, f: Maping): Maping = f WITH [`mp:= lambda(x: Vector[f`dom]): a*f`mp(x)];

o(f: Maping,(g: (same?(f)))): Maping = (#dom:= g`dom,codom:= f`codom,mp:= f`mp o g`mp#)

%------------------------------------------------------------------------------------
% Finally we define the concepts of bijective map and inverse mapping, which are
% given through the same definitions relating to functions, and we also define
% the identity mapping
%------------------------------------------------------------------------------------

bijective?(n)(f: Map(n,n)): bool = bijective?[Vector[n],Vector[n]](f`mp);

inverse(n)(f: Map(n,n)): Maping = (#dom:= n,codom:= n,mp:= inverse[Vector[n],Vector[n]](f`mp)#)

id(n): Maping = (#dom:= n,codom:= n,mp:= lambda(x: Vector[n]): x#)

end linear_map

quality93%

¤ 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.0.14Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

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.

Quellcode-Bibliothek linear_map.pvs Interaktion und PortierbarkeitPVS

Haftungshinweis

Bemerkung:

Quellcode-Bibliothek linear_map.pvs Interaktion und
PortierbarkeitPVS