[FOM] Object-Oriented Formal Mathematical Languages
Victor Makarov
viktormakarov at hotmail.com
Fri Apr 30 11:51:37 EDT 2004
On Thu, 29 Apr 2004 15:00:09 , Jacques Carette wrote:
>As an exercise, you should try to find an adequate OO model of
>the theory of the ring of rectangular matrices, where you can only
>add and multiply matrices of compatible size *at compile time*.
(By the way, there is no such thing, as "the ring of rectangular matrices").
There is some misunderstanding. I am interested in the design of practical
formal mathematical languages. Practical formalization of mathematics is
expressing mathematics, that is, mathematical definitions, statements and
proofs, in a (usually small and simple) formal language with strict rules of
grammar and unambiguous semantics (John Harrison). That is, any such
language has at least the following 3 components:
a) An underlying logic – a formal logical system
b) A sublanguage for writing definitions.
c) A sublanguage for writing proofs.
( One of the most well-known such languages is the Mizar language).
Because we can consider algorithms as definitions of some special kind, we
can use such a language as an algorithmic language.
Object-Oriented Programming Languages (like C++, Eiffel) are very
interesting for the the design of practical formal mathematical languages
(like the Mizar language) because (as Gregory Tseytin stated) "The
fundamental concepts of object-oriented programming like object, class,
inheritance ... belong to description of thinking rather than to programming
techniques" (see http://www.math.spbu.ru/user/tseytin/).
So I am not trying "to find an adequate OO model of the theory of the ring
of rectangular matrices" but rather looking for practical formalisms for
describing mathematical concepts (including the concept of rectangular
matrice).
In my (still very experimental) formalism the concept of rectangular matrice
(over some field) can be described in the following way:
field :: matrice := Matrice | ( rng = elf);
Here:
field - the name of the previously introduced theory of fields,
elf - the name of the carrier set of the field,
Matrice - the name of the general theory of matrices (defined as a heir of
the general theory of functions, so we can use the name rng),
rng - the range of the function - can be used here because Matrice is
defined as a heir of the general theory of functions.
The expression T | P, where T is a theory and P is a formula, denotes the
theory T1 obtained by adding to T the formula P as a new axiom of T1.
T :: A := B means " in the theory T, define A as an abbreviation for B" (the
notation "::" has been borrowed from C++). T is called the host theory for
A.
The concept of general (rectangular m x n) matrix:
Matrix := Function | E[m:nat1!n:nat1, dom = 1..m # 1..n]
That is , a rectangular matrix m x n is such a function, that the domain of
that function is the direct product(denoted as #) of the sets {1,2, ..., m}
and {1,2, ..., n}; (the host theory for Matrix is the Root theory,
introducing basic logical and set-theoretical notations).
There is no problems in defining addition(+) and multiplcation(*) of
rectangular matrices:
field :: +(A:matrix ! B:matrix | A.m=B.m & A.n=B.n) := F[i:1..A.m !
j:1..A.n, A(i,j) + B(i,j)];
field :: *(A:matrix ! B:matrix | A.n=B.m) := F[i:1..A.m ! j:1..B.n, A.row(i)
** B.column(j)];
Here:
F[d, f] - the typed lambda notation,
** - the operation of scalar product of 2 vectors(previously defined).
The "dot notation" (A.n, A.row, ...) has been also borrowed from C++.
Victor Makarov
http://home.nyu.edu/~yvm204/vm/vm.htm
_________________________________________________________________
FREE pop-up blocking with the new MSN Toolbar – get it now!
http://toolbar.msn.com/go/onm00200415ave/direct/01/
More information about the FOM
mailing list