A Conversational System

We have come to think of the configurations/states that exist in the memories of computers as actual objects that 'reside' in a computers memory. In a sense the computers mental models (or maybe 'mental images') of things.

Not to long ago this might have been hard to explain, but today everyone is used to the idea that computers 'contain' emails. Of course it doesn't actually contain anything like a real physical piece of mail, but E-mails and every other thing constructed by a computer system is 'made' out of data objects like numbers (e.g., integers and rationals), characters and strings of characters. Even these are actually just electrical signals but we have come to talk about them as actual things and we propose to do that here. In fact, this is what we do when we talk about a person's 'thoughts'. They are also just electrical impulses in the person's head (our own mental model of these these "other person's" thoughts are likewise just electrical impulses in our head. What data, either primative or structured, might be usable as a basis for a computer's mental models is the ontological component of this work.

To this end we define a collection of finite structures called types. Our 'thinking sytem' will use these types to represent its 'mental models' of things. On the question for any notion we discuss will be "What type of thing is it?" and by this we mean—what data structure could we use as its mental model in our system.

Using types we have the ability to do something that is not available in the usual presentation of ideas, namely we can implement the traditional philosophical difference between use and mention. By adopting the point of view that numbers are actually in the computer, we can actually add two numbers, rather than simply being able to mention the results of this 'addition' in some language. Unlike Prawitz, who explicitly states that there are no well-formed formulas in his book (he only mentions them), we actually can have numbers in our computer. (I like the paraphrase Prawitz as "I see no [wff]s here!!!" - Prawitz x Colossal Cave). the system's memory can contain things it can not mention and thus cannot it cannot speak about these things!!! The question of the extent of the things we can represent using types way is the subject matter of our theory of types. We won't claim that types can act as the mental models of everything but we claim that they increase the scope of the things we can model by a substantial amount over both the languages of logicians and the current modeling languages used by computer researchers.

Everyone today knows how to use a computer. You move your finger or speak to it or click on something or type something and the computer responds by doing something. You type a text message and the computer 'sends' the message to its intended recipient. Sometimes the computer reports something back to you.

As we noted above, we ask; 'What type of thing is a 'text message'? Where is it? How was it 'made'? Where is it now? If it's a thing, in what sense can it exist in more than one place (eg, on both your phone and mine). What do you mean it was sent?

In this work we will call your input to a computer 'typing' even though we know full well that in today's world you frequently interact with your cell phone (i.e., computer) by using a touch screen directly or even by speaking to it (a la Siri on an iphone) as opposed using a keyboard. We think of your interaction with your computer as a dialog between you and it. It's conversational and the what makes a successful product is whether the 'quality of conversation' you can have it is rich enough to be useful.

We can formalize the idea of a conversation by introducing the idea of an interpreter (a technical term of computer science). An interpreter is a computer program that repeatedly 1) interprets what you tell it 2) does something (not always visible) and 3) sometimes prints (i.e., types back at you) a response. Computer scientists call this a read-eval-print loop REPL).

When describing this kind of dialogue we write:

$<text we type>
<response typed by the computer>

where the '$' is typed by the computer to remind us that it is listening. This 'prompt' may be different for different computer programsn and is usually called "the prompt".

Interpreters are NOT like functions. They have inputs and outputs and the do other things than simply provide answers. We introduce the idea of a computation system to describe what a computer can do. By asking "What is the type of a 'computation system'?" we explicitly mean: how do we describe it as a type (ie, a finite data structure that can exist in the memory of a computer).

  Our goal is to explore the idea of having a conversation with a computer.
  At this time we beg the question of speaking, touching, seeing, mousing, ...
  We simply type 'expressions' and it types 'expressions' back
  The important idea to come away with is
    We can ask the computer to do things and to remember what its done
    We can ask the computer make an agreement with us about
      how we are to mention what we have already discussed

The computation systems that interests us will have to be able to mention ALL types of objects.

Computation Systems come with well defined ways of mantioning basic data. In this note we will only mention a few.

boolean values
integers
rationals
characters
strings
symbols
lists
sexps

Mentioning a basic type is simply an exercise of recognition,

$1
1
$

This means that when we type '1' the computer simply says yes I recognize what you have mentioned and I can say it back to you. In this case we implicitly ask "Do you have an understanding (a meaning) for the numeral '1'" and the computer replys yes and when I mention that thing to you I will call it '1' (the numeral). We can only hope that the computer is 'thinking' of the number one.

The same idea for

$2309498524523478728474935863485769348568943576485634985674586
2309498524523478728474935863485769348568943576485634985674586
$

Now we come to a subtle point. Not all computation systems may understand 2309498524523478728474935863485769348568943576485634985674586. A real computer will run out of memory and even if it could understand this the number mentioned by this numeral it probably wouldn't understand a numbral that had 2309498524523478728474935863485769348568943576485634985674586 digits!!!. So clearly our computer (like our brain) has a limited capacity and could NOT possibly represent 'arithmetic' as imagined by Peano (or any of the usual thearies of arithmetic)!! So what's in there? and how do we theorize about it? And to ask our now annoying question—"what is the type of this theory?" or more pointedly "What is the type of a 'theory'?" We come back to this below. Here we are discussing computation.

To explain the notation below we introduce two additional types of basic data: symbols and lists.

We mention a symbol by using a bunch of characters. In its simplest form a symbol is mentioned using what we might call a word (or technically its print-name or pname).

$asdfg
asdfg
$

In practice print-names are more complicated and depend on the computation system. We leave the details to {ref}. Notice that unlike mathematical practice by a symbol we mean an ordered bunch of characters not a single characters distinuished by font. The pname is how we mention symbols. An actual symbol (in a computer) may be quite a complicated structure. Here again the utility of having both things and their descriptions simultaneously available is an importabt feature. (Of course a logician will say that if you have arithmetic we cn use Godel numbering to create 'numerals' for almost anything BUT in practice this is not a very natural, reasonable or usable alternative. {{Feferman had a phrase for this (maybe something like "being ale to carry out sustained reasoning") }})

We may ask the computer to remember something:

$(SET X 3)
3
$

This could be paraphrased as "Please remember that when I meation X you should think of the numbet 3."

Here we need to be a bit more careful. In normal speaking and writing there are no numbers—only numerals. This case is the same. We 'mention' the question and the computer 'mention's the answer!!!! When we type '(SETB X 1)' we are doing something quite complex. The characters SETB formalize is a eequest to remember something and we propose to use X whan we refer to it in the future. In addition we are telling the computer that we will use the word X to refer to the number mentioned by the numeral (character(s)) '3'. Of course if I were not being so careful I would have simply written "we will use X to refer to the number 1", which abuses notion by using '1' to 'be' the number one, but of course I wrote the character '1' which is actually a numeral.

So we can only write (type) and say 'expressions' which can only mention things. (Thus Prawitz "I see no WFFs here") In the case of out interpreter '(SETB X 1)' is a particular type of expression called an's-expression or [sexp]. We define [sexp] formally in {ref}

list-mak is the name of a function that takes some values and returns the list of them.

$(list-mak X 1)
(3 1)
$(list-mak 1 X)
(1 3)
$

Some SEUS functions return multiple values. listUN takes one argument and if it is a list returns its elements as a bunch of values. In the usual way <thing> is an abbreviation for the QUOTE form (QUOTE <thing>), and it evaluates to <thing>.

$(listUN X) 
SEUS-ERROR wrong number of args listUN 

listUN takes one argument of type list, not three arguments. Therefore an error is reported.

(listMK (listUN L1) (listUN L2))