Representations

Any reasoning system that includes to ability reason about the data structures
that were used to build it (e.g., sexpressions in LISP) and at the same time
imagines that there are other things in the world (eg dogs or 'your mother')
and uses these structures as the mental models of things has to address the
problem that there are not enough 'things' available to model this situation.

To be more explicit, if the recognizer you define for [data-structure] is 

  (DEFUN DATA-STRUCTURE? (obj) 'TRUE')

(i.e., every mental model is a [data-structure]) then if a theory mentions
both [data-structure]s and other things (e.g., persons - 'your mother') will
have as a consequence that everything is a [data structure]. This is unlikelywhat what you expected.

In an early version of the FOL system (1977) this actually happened to us
when we tried to imagine that [natnum]s (natural numbers) were disjoint 
from LISP [sexpression]s in a theory where we had both the axioms of LISP
and the axioms of Peano arithmetic and had assumed that [data-structure]s
and natural numbers were disjoint.  To our surprise the interpretation of  

   (SEXPRESSION? One)

was TRUE!!! and our theory didn't express our intensions. (The individual
constant symbol 'One' in this context was defined to mean the second
natural number (the successor of zero.)  Sadly enough, the axiom that
easserted that sexpressions and natural numbers were disjoint rendered the
context inconsistant.

Solution
--------

The solution we adopted was to introduce representations.  Some 
documentation of the original solution can be found in [Weyhrauch 1977].
Our latest version is part of IBUKI tyupe theory, where we have introduced 
the type [representation] as a type of IBML Data to uniformly deal with
this problem.  The idea is, that however IBML types are implemented in an
actual computer environment, the data structure needs rich enough to 
distinguish model itself as well as other things and programs need to
be able to recognize the difference. This is accomplished by using the  
[data-type] which we call [tag], that allows us to distinguish some data
as the models of [basic-data] and others as models of other things. Tagged
data tells us whick is which.

The theory of IBML Data thus satisfies the following

  (FORALL obj (iff (MENTAL-IMAGE? obj) 
                   (OR (REPRESENTATION? obj) (BASE-DATA? obj)) ))

History

The ability to use 'representation' was extended to functions and relations,
which were first described and developed in the FOL system by Chris Goad,
who later founded thr company Selma which commercialized
these ideas.  Later Dave Posner (at the company Encirq) incorpretated these
ideas into their database product, where he called the functions that did 
automated data format translations of SQL queries 'Goads'. The need for this
ability reappears when we formalize the metatheory of types, which is
the origin of the current invocation.