[FOM] Object-Oriented Formal Mathematical Languages

[Jacques Carette]

Brian Postow <bpostow at union.edu> wrote:
> Dennis E. Hamilton spake:
> 
> > An important difference between OOP objects and mathematical (systems of)
> > objects is that OOP objects have states and history behaviors and so do the
> > OOP objects that are supplied to their methods for usage.
> 
> I think that this is probably a very important statement. Most
> programming paradigms have state, and directionality of time. 

I completely agree.

> Most of
> the foundational mathematics that I know is bi-directional. It
> involves relationships between structures, but if these relationships
> hold, then they always hold and always will. The PL concept of "side
> effect" is not present in most mathematical systems. This is why the
> lambda calculus and functional programming are most closely tied to
> FOM ideas.

If one takes this relational view of mathematics, with which I am quite partial, then the (higher-order) logic 
programming paradigm, as seen in for example lambda-prolog, is even more natural for mathematics.  Lambda calculus and 
functional programming are very good at capturing the computational structures present in mathematics, much less so 
the pure relational structures.  The trouble with raw prolog is that only first order relational knowledge can be 
adequately captured, which means that all the functional aspects of mathematics are awkward.  In other words, too much 
generality (only relations) makes it difficult to conveniently capture 'functions', where not enough generality (only 
functions) makes it impossible to capture purely relational knowledge. 

 From that point of view, programming systems like Mercury, and to a lesser extent Maude and HOPS are all quite 
interesting.

Once one strips away the over-reaching claims, Goguen's and his colleagues' work on Institutions, Hidden Algebras and 
so on also contains some intriguing ideas that bring models of computation and models of mathematics closer together. 
 The systems OBJ3 and CafeOBJ are the results of those ideas - also worth a close look.

Jacques