Mutable Data

This note is about [mutable-data] and the difference between [mutable-data] and [immutable-data]. The use of mutable data in computer applications is taken for granted but this commonplace idea has not had any real impact on the formalisms of logic or the discussios of philosophers. The purpose of this note is to illustrate the idea of mutable data. We show how IBUKI uses these structures to uild reasoning systems in [???].

The behavior of both imutable and mutable structures is well defined but their theories are quite different. [immutable data] corresponds to what we normally formalize using extensional ideas. [mutable data] is defined and formalized relative to an environment and is prima facie more complicated to formalize.

A tutorial on mutable data

As mentioned above most programmig laguages use mutable data all the time. Perhaps the most usual kid is array where the contents of the array are allowed to be updated at any time. This has the consequence that programs are not in general fuctioal, i.e., for arrays a1 and a2, a1 can equal a2 but (f a1) may not equal (f a2)!!!. We will explore this i more detail y usig [pair]s as a example.

A [pair] is a structure that has two parts. for historical reasons called 'car' ad 'cdr' (or 'left' snd 'right' if you prefer). We write a [pair] as (A . B), where A is the 'car' and B is the 'cdr'. Here A and B ca e any objects byou wanr.

Immutable [pair]s

  (pair-mak a b) = (a . b)
  (pair-get-car (a . b)) = a
  (pair-get-cdr (a . b)) = b

  and

  (pair-mak (pair-get-car p) (pair-get-cdr p))  = p
  (IFF (= (a . b) (c . d)) (AND (= a c) (= b d)))

Taken together the last two formulas characterize the essenntial properties of an immutable [pair].

Mutable [pair]s

oe way to visualixe mutable [pair]s is to think about them as two mailboxes in an old fashioned post office. The boxes are used to store mail. And there is a natural division between the mailbox and its contents. I addition, we need to be able to locate the two boxes. We use a picture to trepresent this idea

boxes and arrow here

We now introduce two updating operatios:

  (pair-set-car p obj)
  (pair-set-cdr p obj)

which modify the 'car' and the 'cgr' of a [pair]. If p = (a . b) the the result of pair-set-car to oj is (obj . b) and the result of pair-set-cdr is (a . obj). Note these are not fuctions i the mathematical sense.

If you think of a [pair] as [immutable-data]
  the properties of types and data in the corresponding FOL contexts
If you view a [pair] as [mutable-data]
  is used in SEUS environments for doing computations
   and are compatible with the 
     IBML types for [seus-data]  AND
     the formalization of SEUS as a computationsystem in an FOL context

The theory of [mutable-data] can be replaced by a theory of
  [immutable data] but real computations
    1) use [mutatable-data] all the time  AND
    2) computations on real computers do I/O
       which de facto do not behave like functions.
  A usefuk computation theory must account for this

IBUKI Data is by definition [mutable-data]
  The use of LISP to implement IBUKI Data conviently makes this the default
  programs on IBUKI data are either
    functions that treat the data as immutable
    operations that can change the content of their args

SEUS uses the IBUKI Data and thus [seus-data] is mutable

Operations on [immutable data]
  can only look at a datum or make a 'new' one
    (EQUAL A B) - (EQ A B)
       -get-
       -rem-
    (EQUAL A B) - (EQ A B)

Operations on [mutable data]
  destructively change data leaving args EQ to before
    (AND (EQ A B) (EQUAL A B))
       -set-
       -del-
    (EQ A B) but not (usually) necessarily (EQUAL A B)

Mutale data if fiite.

Circular Structures

Determining if a Datum is Circular

Printing and Reading Circular Data

Copying a Circular Structure

Constructing Data

THEOREM: All constructios are finite.
THEOREM: All [data] in a haed has a construction.

Paths

THEOREM: All paths are finite
THEOREM: The previous theorem is expressable ad proveable in the first order
mets theory of the cotext 'Data'.

THUS the two cotexts. Data and MetaData, take together show the theory
of arithmetic is catagorical.