[FOM] Object-Oriented Formal Mathematical Languages

[Victor Makarov]

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/