Scheme in Dr. Dobb's
Author Message
Scheme in Dr. Dobb's

Quote:

> I just received the latest copy of Dr. Dobb's Journal that came with a
> supplement called "Software in the 21st Century." The supplement contains
> an interesting article titled, "New Languages, Old Logic: Old Ideas Form the

it's online at

Proofs are Programs
http://www.*-*-*.com/
http://www.*-*-*.com/
19th Century Logic and 21st Century Computing
Bell Labs, 2000

take it as an appatizer and then during christmas-break
treat yourself to

Lectures on the Curry-Howard Isomorphism
ftp://ftp.diku.dk/diku/semantics/papers/D-368.ps.gz
ftp://ftp.mimuw.edu.pl/People/urzy/errata.ps.gz
Morten Heine B. S?rensen and Pawel Urzyczyn
University of Copenhagen, 1998

or

The Evolution of Type Theory in Logic and Mathematics
ftp://ftp.win.tue.nl/pub/techreports/laan/proefschrift.ps.gz
ftp://ftp.win.tue.nl/pub/techreports/laan/errata.ps.gz
Twan Dismas Laurens Laan
Eindhoven University of Technology, 1997

happy holidays !

Mon, 28 Apr 2003 09:50:17 GMT
Scheme in Dr. Dobb's
The Evolution of Type Theory in Logic and Mathematics
ftp://ftp.win.tue.nl/pub/techreports/laan/proefschrift.ps.gz
ftp://ftp.win.tue.nl/pub/techreports/laan/errata.ps.gz
Twan Dismas Laurens Laan
Eindhoven University of Technology, 1997
happy holidays!

with interest. I am creating a webpage about Skolem,
Diophantine equations, lambda calculus, Godel, Turing
which deals with the primitive origins of programming
languages, incompleteness and randomness.

Because of your interest in the topic I would like to ask
you a few questions. I gathered the following information
from the Nordic Journal of Philosophical Logic and in
particular the article by Herman Jervell which in part:

Diophantine equations and logic
I believe that Skolem considered Diophantine equations and
logic as one subject. Let me indicate a little speculatively
how Skolem's thought might have been. The theory of
satisfiability of equations like

4x^3y^4 +3y^3 -13z^5 = 0

This is really not far from questions about satisfiability of
logical statements. A statement can be seen as a
Diophantine equation'' where we have

true             1
false            0
not F          1-F
F and G     min(F,G)
F or G       max(F,G)

In addition, we have to indicate how the quantifiers are to be
interpreted. This is of course more complicated. So Skolem's
first work was to see how the quantifiers could be interpreted.
________________________________________________

Skolem in fact gives two systems: One for defining objects,
objects defined by primitive recursion, and one for proving
properties of such objects. This would be quantifier-free
statements with free variables, and with the possibility of
proving theorems using (quantifier-free) induction. These
two systems were developed in parallel. Skolem was able to
develop a substantial part of number theory. For example,
prime numbers were introduced.

Here Skolem comes very close to problems in contemporary
computer science. Let us for the moment skip over the fact
that Skolem considers only natural numbers. His two systems
could be considered as a programming language--for defining
objects--and a programming logic--for proving properties
about the objects. This is in fact of great interest for
contemporary computer science. Especially so if data
structures other than natural numbers are admitted.
Skolem's idea works equally well for data structures with
more than one base element and more than one generator.
--And so we are in business, with an interesting programming
language and its corresponding programming logic. I believe
that Skolem would have considered this as the same idea as
in 1923a. (Below is a reference starting with subtopic#3)
^^^^^^^^^
http://www.hf.uio.no/filosofi/njpl/vol1no2/pioneer/index.html
_______________________________________________

1. Are you familar with the content of  "1923a" mentioned above?

Next in reference to my website:

I want to be able to say something which is correct, probably known
by experts, but which is accessible to the general reader and might
surprise the semi-expert comp.ai.philosophy denizen.

Which is that Diophantine representations can be utilized as a
simple programming language with equal computation capacity to
the other acknowledged equivalent computational approaches.
(even if it would be more difficult){end of quote}

I received a clarification/approval in email correspondence:

"In fact every RE set, A, can be defined as:

A = { n | for some i, a(n, i) = 0}

where a(n, i) = 0 is a Diophantine equation.
The reverse statement is also true.

We can turn Diophantine equations into a
computational language if for each
Diophantine equation, a, we add a
search operator, mu, such that

mu(a, n) = the smallest i such that a(n, i) = 0

Of course mu may not always find an i, which is
what prevents Diophantine equations from being
totally recursive. {end of his reply quote}

Quote:
SH writes:

So I think this is a confirmation and he is commenting
that this may not terminate unlike primitive recursion.

I am not sure what "we add a search operator, mu,
such that mu(a, n) = the smallest i such that a(n, i) = 0"
(^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^)
means exactly. I came across this from mu-calculus

Set
is a group of articles that results from a search command.
Operators can act on sets or words.
We obtain finitary complete axiom system for the $\mu$-caculus.
It can be roughly described as a system for propositional modal
logic with the addition of a induction rule to reason about least
fixpoints.

2. Could you clarify this? Does least fixpoints = "the smallest i"

3. This would mean that a Diophantine representation could
be used to implement a program which would prove theorems?

4. How would you philosophically characterize the evolution
of mathematical logic from an agenda to have a complete formal
basis for mathematics to ever stronger results of incompleteness
which now appear as randomness in Chaitin's omega variable.
Any thoughts about the connection between randomness and Inc.?

5. Would you consider Diophantine equations a meta-language?

Resolution and Discovery,
Stephen

Sent via Deja.com http://www.deja.com/

Tue, 29 Apr 2003 03:00:00 GMT
Scheme in Dr. Dobb's

Quote:

>   Proofs are Programs
>   http://www.ddj.com/articles/2000/0013/0013g/0013g.htm
>   19th Century Logic and 21st Century Computing
>   Bell Labs, 2000

from the original term, and that Scheme "got lambda right".  How so?

--
vsync
http://quadium.net/ - last updated Fri Nov 10 03:41:55 PST 2000
(cons (cons (car (cons 'c 'r)) (cdr (cons 'a 'o))) ; Orjner
(cons (cons (car (cons 'n 'c)) (cdr (cons nil 's))) nil))

Wed, 30 Apr 2003 08:55:07 GMT
Scheme in Dr. Dobb's
+---------------
| >   Proofs are Programs
| >   http://www.ddj.com/articles/2000/0013/0013g/0013g.htm
|
| from the original term, and that Scheme "got lambda right".  How so?
+---------------

I suspect that he's referring to lambda variables in early Lisps
being dynamically scoped, and in Scheme being lexically scoped.

But that's moot now, since Common Lisp is lexically scoped, too. [*]

-Rob

[*] Well, unless you shadow an existing dynamic variable, in which
case your "lexical" variable suddenly becomes a dynamic variable.
This is why the CL guys are *so* careful to textually flag global
variable names with those asterisks, since there's really no way
in CL to declare a top-level lexical variable. [Well, except with
some tricky symbol-macro hacks...]

-----

Network Engineering             http://reality.sgi.com/rpw3/
Silicon Graphics, Inc.          Phone: 650-933-1673
1600 Amphitheatre Pkwy.         PP-ASEL-IA
Mountain View, CA  94043

Wed, 30 Apr 2003 12:41:41 GMT
Scheme in Dr. Dobb's

Quote:

>> I just received the latest copy of Dr. Dobb's Journal that came with a
>> supplement called "Software in the 21st Century." The supplement contains
>> an interesting article titled, "New Languages, Old Logic: Old Ideas Form the

>it's online at

>  Proofs are Programs
>  http://www.ddj.com/articles/2000/0013/0013g/0013g.htm
>  19th Century Logic and 21st Century Computing
>  Bell Labs, 2000

>take it as an appatizer and then during christmas-break
>treat yourself to

>  Lectures on the Curry-Howard Isomorphism
>  ftp://ftp.diku.dk/diku/semantics/papers/D-368.ps.gz
>  ftp://ftp.mimuw.edu.pl/People/urzy/errata.ps.gz
>  Morten Heine B. S?rensen and Pawel Urzyczyn
>  University of Copenhagen, 1998

>or

>  The Evolution of Type Theory in Logic and Mathematics
>  ftp://ftp.win.tue.nl/pub/techreports/laan/proefschrift.ps.gz
>  ftp://ftp.win.tue.nl/pub/techreports/laan/errata.ps.gz
>  Twan Dismas Laurens Laan
>  Eindhoven University of Technology, 1997

>happy holidays !

--
--------------------------------------
Farkas Gy?rgy
Budapest

--------------------------------------

Sat, 03 May 2003 03:00:00 GMT

 Page 1 of 1 [ 5 post ]

Relevant Pages