SUO: Re: Logic & Programming Languages
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
| Can you tell me, Socrates, whether virtue can be taught,
| or is acquired by practice, not teaching? Or if neither
| by practice nor by learning, whether it comes to mankind
| by nature or in some other way?
|
| Plato, 'Meno'
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
John F. Sowa wrote:
>
> Following is a question I received and my response to it.
> I'm sending this note to these mailing lists, since there
> may be other people who are also interested.
>
> John Sowa
> __________________________________________________________________________
>
> > What you say on page 12 of your book caught my eye,
> > and I have a question about it that I am hoping
> > you may be able to help me answer.
> >
> > You say:
> >
> > "Perhaps there are some kinds of knowledge that cannot be expressed in logic.
> > But if such knowledge exists, it cannot be represented or manipulated on any
> > digital computer in any other notation. The expressive power of logic includes
> > every kind of information that can be stored or programmed on any digital computer.
>
> Just take any program P that is executed by any digital computer C to
> transform input data D1 into output data D2:
>
> 1. The instruction set of C can be formally defined in logic, and
> an interpreter for those instructions can be written in logic.
>
> 2. The program P is a sequence of instructions with conditional loops.
>
> 3. There are formal methods for translating P into a logical expression,
> which combines subformulas that represent each of the instructions in P
> into a single (very large) formula.
>
> 4. Then replace each formula with its definition in logic.
>
> 5. Combine that formula with the formula that defines
> the interpreter for instructions in C.
>
> 5. The result is a single giant formula that expresses exactly
> the same transformation from D1 to D2 as the program P.
>
> Of course, this is a rough outline, but each of the steps
> has been analyzed in detail in the comp. sci. literature.
> The resulting formula is huge, and nobody would really want
> to use it for any serious computation, but the fact that it
> can be formally generated is an existence proof of the claim:
> anything that can be computed by any digital computer can be
> formalized by a statement in logic.
>
> > I'd be grateful for any elaboration you care to offer.
> > If it's more convenient, feel free to point to references
> > that might help. You needn't dig up all the details of the
> > references; I'm usually pretty good at finding things with
> > partial information.
>
> The references can be found in work on formal automata, programming
> language semantics, and other fundamental texts in computer science.
>
> If you use Google, you might try typing the following keywords:
>
> 1. To get information about Tony Hoare's axioms for programs,
> you'll get about 1,820 hits with the following keywords:
>
> hoare axioms
>
> 2. For information about the Church-Turing thesis
> that everything computable can be computed by
> a Turing machine, the lambda calculus, or
> recursive functions (all of which can be
> defined in logic), the following keywords
> will give you another 5,680 hits:
>
> church turing thesis
>
> 3. For automata and formal languages,
> the following will get you about
> 30,100 hits:
>
> automata formal language
>
> Hint: Many of the hits are course descriptions posted by instructors at various
> universities. Those descriptions will often lead to a course syllabus, reading
> list, or other useful background information. So you can try following them up
> for further references and techniques.
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
John, & Programmar Pilgrims Alle ...
Loci Classici: Plato's 'Meno' and 'Sophist'.
Here we find the ultimately periodic question
"Whether Virtue Can Be Taught", which I began
looking into 2^2^2 years ago and was shocked
to recognize that it constituted the ancient
precursor to the Turing Test. Even the form
of the 'Sophist' has a recursive structure.
One of the problems that Peirceans have in explaining
how semiotics is a broader, more general subject than
logic is that the receiver of its avowal is naturally
prompted to ask: But how can I reason, or think well,
about anything at all, much less signs, without using
logic? But that is like asking: How can I speak or
write at all without having a formal grammar of my
native tongue within my utter grip and quick grasp?
Here is where the classical distinction, echoed by Peirce,
between "logic as taught" and "logic as used" chimes in.
Contemporary ears may strain to hear some reverberant
echo of this note in Chomsky's competence/performance
distinction, but its chord is really struck by that
tension among competence, performance, reflection.
Or so I hear,
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤