The Monkey Trials

We didn’t do justice in class to section 6.2 of the class text, Decidablity of Logical Theories. So here’s the story.

A Logical Theory contains relations, variables, logical connectives, and quantifiers. The logical connectives are always AND, OR and NOT, and the quantifiers are always EXISTS and FORALL. These elements are combined into formulas in simple ways conforming a simple grammar. It is easy to tell what is a formula, because the grammar rules are simple. How simple? It must be decidable. In addition, there are axioms, which are formulas which are known to be a priori true.

For instance, the theory of addition would have a single relation PLUS, which given three numbers x, y and z, would be true if and only if x+y=z, at least that’s what we would picture in our minds. A model for a theory is a map of the relation to some “real world” example such that all the true relations and formulas in the theory are actually true in the real world. So the theory of addition would certainly be true in the model where the variables would take values in the integers, or naturals, and PLUS would agree with addition of integers.

The theory of addition would have axioms asserting the properties about the theory, such as the commutativity of addition, the existence and uniqueness of the sum, and (perhaps) of the zero element. These axioms would be chosen so that they capture accurately the properties of the common model. The axiom of commutativity would be:

• FORALL x, FORALL y, EXISTS z PLUS(x,y,z) AND PLUS(y,x,z)

It is possible for multiple models to exist. Addition over the integers has the same formal properties as addition over the integers mod N (except the set of elements is finite and there is no order relationship … neither of these is important to the theory), or addition over the reals (except that the reals have a continuum of elements, while the integers are denumerable - again this is not important to the theory).

The question is, is the set of all true formulas of the theory Turing Decidable? For some theories, it is, for others, it is not. For those, this means that there is no algorithmic method for deciding the truth of all propositions. Since Proof is an algorithmic method, this means that not all truths are provable.

If we restrict to a theory modeled by the integers and addition, this is decidable. However, if we consider a theory modeled by the integers, addition and multiplication (called the language of Number Theory), this is not decidable. Because, given a description of a Turing Machine M, and an input w, it is possible to write down a formula in the language of integers, addition and multiplication, such that the formula is true if and only if M accepts w.

It’s a bit of a trick to do this, but in a certain way, I’m not surprised. The amount of brains needed to run a Turing Machine (move left, move right, write a zero, write a one) doesn’t seem to be more than what’s needed to solve integer formulas! And indeed, it isn’t.

The set of true formulas is, however, Turing acceptible. The true formulas are those true because they are axioms, or are relations, or are formulas whose truth is entailed by logical consequence from the axioms and relations. Such truth formulas will be true in any model of the theory. It is possible that certain formulas will be true in some models and not others. This occurs when essential axioms are removed. For instance, a theory of geometry with the parallel postulate removed. Euclidean and non-Euclidean geometries are models for the neutral theory.

Not withstanding that, it is possible to write down the entailment rules so that a diligent Turing Machine can apply the entailment rules to the axioms and grind out many true formulas, and these are called theorems, and the grinding process is called proof. Rather un-poetic, but there you have it.

Due for Monday, April 2, Phase I of a TFTP Client/Server. Phaser I will implement:

1. Recognition of command line options.
2. Start up of server binding to port given in command line.
3. Datagram construction of RRQ and WRQ by client, and sending UDP packet to server.
4. Decode of RRQ and WRQ packet by server and dump to stdout.
5. New socket and binding to TID by server for response to client.
6. Datagram construction of ERR by server, and sending UDP packet from TID to client’s sending port.
7. Decode of ERR and dump to stdout of client.
8. After which, client and server programs exit.

Use stdin/stdout piping, rather than named files. However the RRQ and WRQ should implement the protocol, so use stdout and stdin as the filenames in the WRQ and RRQ packets, respectively.

The command line syntax is mytftp -s portnumber for server, or mytftp [-g|-p] host:port for server. If the command line is wrong, print a help. Eventually you will have additional command line switches for NETASCII vs. RAW, and for debug.

The Computer Networking course covers a lot of ground. We can only touch superficially on a lot of topics. Just the same, it is probably good to get some idea of how things work, to build up a stock of experience with particular networking technologies, and to have some practical knowledge that might help out in the real world. With the apology to superficiality, I now describe what I know about a Layer 1 and 2 networking protocol affectionally called WiFi.

Read more »

Victor will be teaching next week on the 12 and 14-th. The 16-th will be off.

Homework 1 posted to homepage. Exercises are about notation and simple set theory, and there is one proof to do.

We began the course by looking at Finite State Automata. We will discuss these for awhile, and in doing so introduce the formalism-to-live-by for this course.

We introducted networking by just messing around with ping and traceroute; and the next class, looking at how to program simple network services.

Big ideas introduced included packet versus connection networking, client-server discipline, and to some extent the layering of communications according to next-hop and long-haul communication tasks.

This course meets MWF 1:25- 2:15 PM in Memoral 300.

This course meets MWF 3:35- 4:25 in Memorial 300.

Regarding the issue of software engineering, we are reading a selection of works devoted various operating systems. The Cathedral and the Bazaar is about several things,

1. The Linux development model
2. The Sociology of the Linux development community
3. Hints of Software System Design

The Cathedral refers to the traditional software development practice, quoting from the paper: cathedrals … caefully crafted by individual wizards … working in isolation … with no beta to be released before its time. To me, it also means a command and control, and a development process beginning with requirements, through planning, and finally coding. This is the Microsoft way, presumably.

Linux development is the Bazaar. The elements of the Linux development model are:

1. Release early, release often.
2. Delegate everything.
3. Be Open.

There is also the aspects of rewriting and reuse, rather than innovation, that is, to have cycles of working from existing code to improve it; and the aspect of using users as co-developers, that all ideas and improvements come directly from the user community, not to dictate or predict.

The paper is also about the sociology of open source and how it supports the Linux development model. There are three aspects to the sociology, some of which could also be termed psychology.

1. Concerning the group comprising the Linux hacker community.
2. Concering the individual user or hacker.
3. Concering the leader of Linux, or more generally, of an open source project.

Remarks on group dynamics include the famous Linus’ Law, also known as the Many Eyeballs theory: given enough eyeballs, all bugs are shallow.  This is contrast to Brooks’ law which claims that the more programmers the slower the project, due to interaction and coordinate costs. One mystery of open source is why Linus’ Law holds, rather than Brooks’.

Concering the individual user or hacker, motivation according to egoboo, a currency of peer respect, is considered. Qualities of the leader, Linus, are discussed, primarily his delegation model, his ability to encourage participation, his ability to moderate, not dictate.

Raymond became a central figure in open source when it became part of the planning committee to make the Netscape browser open source. Since then several important software projects have adopted an open source model.

Quoting Wikipedia: Open source describes practices in production and development that promote access to the end product’s source materials—typically, their source code.