| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/linear_algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle linear_map.pvs Sprache: PVS |
|||||||||
|
% --------------------------------------------------------------
% 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) *(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]] id(n): Maping = (#dom:= n,codom:= n,mp:= lambda(x: Vector[n]): x#) end linear_map ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28