Re: Universal grammar

In article <haberg-2610061517270001@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
Hans Aberg <haberg@xxxxxxxxxx> wrote:
In article <1161866092.431188.312330@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>, "Rob
Freeman" <groups@xxxxxxxxxxxxxxxxxxx> wrote:

...................

Perhaps like this. I think I know how to build a representation which
would give you the information you need to parse proofs reliably.

It is though very difficult to build a reliable theorem prover. :-) Bound
variables are the problem.

Reliability is not the problem. It is utility which is.

Tarski showed how to build a theorem prover for systems of
equations and inequalities in real numbers. We just cannot
make it fast enough to do much good.

We have reliable proof checkers; it is not hard to tell if
a formal proof is correct or not. In some cases, theorems
have been proved by machines which could look up enough to
handle an adequate amount of grunt work. A computer did
show that the weakening by Robbins of Huntington's axioms
for a Boolean algebra worked, but it was told how to look.
The only proofs of the four color theorem used computers
to check if an adequate number of special cases could be
handled by four colors; it was humans that checked that
these special cases were sufficient.

Proofs in "object" or "working" maths too, i.e. a way to "overload
symbols" automatically, in the right way. As I say, the representation
would be based on strings, not rules (or ASTs.) But unlike rules it
would be universal.

Overloading is highly used, but needs care and judgment.
The latter is totally missing in computers.

So called name overloading is in pure math formally only a sloppy way to
notate; the Bourbaki <http://en.wikipedia.org/wiki/Nicolas_Bourbaki> team
calls this kind of construction "abuse of language". For example, a +
b,wouldproperly be written a +_R b, etc.,depending which ring (number
system) R one is using. They will get different trees. If there is enough
syntax information, the ambiguitycan be resolved, by syntax or context.

It is just speculation at this stage, but it might be interesting to
follow up.

So I think you try to prove that "strings are better", which I do not think. :-)

--
Hans Aberg


--
This address is for information only. I do not claim that these views
are those of the Statistics Department or of Purdue University.
Herman Rubin, Department of Statistics, Purdue University
hrubin@xxxxxxxxxxxxxxx Phone: (765)494-6054 FAX: (765)494-0558
.

Relevant Pages

  • Re: DICE II Firewire Driver Settings
    ... But I think that part of the problem is that people have been sold on the idea that what used to be too expensive for individuals is now well within their means. ... The one used when the tuner knob fell off? ... I think they make modern computers look good. ... A friend of mine's wife wanted to have Lasik eye surgery, and my friend, a very good engineer, told her to ask the surgeon what sort of software reliability design methods and testing were used on the equipment. ...
    (rec.audio.pro)
  • Re: Formalizing all of mathematics
    ... reliability or even yields absolute truth. ... By "formalizing mathematics" I do ... not understand doing math on computers but doing math in a formal way. ...
    (sci.math.research)
  • Re: MacBook Air Probably Most Reliable
    ... The fact that it has a solid state HD rather than a ... be better for reliability in the short run. ...
    (comp.sys.mac.advocacy)
  • Re: PC based lighting... Re. Diagnosis of Dead Desk
    ... >> computers, and I have downloaded a couple things. ... >> download for free). ... This has what to do with the reliability of a PC as a ... lighting controller, its a practical thing to do. ...
    (rec.arts.theatre.stagecraft)