Rick, (01)
I am *very* strongly in favor of bringing more logic into computer
science, artificial intelligence, and software design and development.
And I am constantly fighting an uphill battle to get people to admit
more useful applications of logic in computer systems. (02)
I am always delighted whenever anyone shows me a fascinating new
application of some branch of math or logic that had hitherto
been neglected. (03)
On the other hand, I also believe that it is important to seek
the simplest structural foundations for our computer software.
Whenever we find complex systems and theories, it is important
to search for a way to simplify them. (04)
JFS
>> As Pat emphasized, there is a huge semantic difference between
>> quantifying over relations (which can be done in Common Logic
>> with a first-order style of semantics) and the kind of higher-order
>> logic that logicians have been kicking around. (05)
RM
> John, your point is completely superfluous. I have already clarified the
> term in relation to section 3.4.4 in Chris's paper. (06)
The point I was trying to emphasize was noted by Quine in 1953.
I wasn't claiming novelty. But note what Pat said (07)
PH
> I have been taken to task by some very competent logicians for calling
> CL first-order, as they are using a purely syntactic criterion of order. (08)
Even professional logicians may need an occasional pointer to literature
that they overlooked or under-appreciated. (09)
RM
> As an aside, why do you say 'kicking around?' I am left with the
> impression that you don't respect the work of these logicians
> on higher order logic. (010)
I have a very high regard for the pioneers in logic in the late 19th
and early 20th centuries. I used to subscribe to the J. of Symbolic
Logic in the olden days, but I got bored with one dissertation after
another that took some point about countable sets and generalized it
to higher and higher orders of infinity. (011)
When I was at IBM, I knew some people at research who wanted to do
nothing but "kick around" their PhD dissertations until they got
them right. And they refused to get their hands dirty by relating
their theories to anything that might have useful applications. (012)
JFS
>> In fact, many logicians have now come to believe that the infinite
>> hierarchy of relations, relations of relations, etc., which are
>> assumed for higher-order logic, should *not* be considered part
>> of logic. They should be considered a version of set theory. (013)
RM
> Really, I hope they are still employed. (014)
I don't understand what point you're trying to make. Russell hoped
to reduce all of math to logic. In order to do that, he wanted to
call the hierarchy of domains part of logic. But the more common
opinion today is that there are multiple possible foundations for
math, and it is better to distinguish the logic and the ontology. (015)
JFS
>> In fact, HOL uses a semantics that is
>> very similar to CL. (It's probably a subset of CL semantics, but
>> it would be necessary to check that claim.) (016)
RM
> Are you referring to Mike Gordon's HOL, or Paulson's Isabelle/HOL? (017)
That entire family use essentially the same logic, with minor
variations. In order to keep their proofs tractable, they do not
let the theorem prover wander aimlessly through an open-ended
hierarchy of infinities. For a history of the family, see (018)
http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf (019)
RM
> Will you be publishing your proof in the Journal of Symbolic Logic?
> This is surely a publishable result. (020)
Doing the exercise of mapping one or more variants of HOL to CL would
be useful. There are undoubtedly many details to be checked. But it
wouldn't be a deep theoretical issue. (021)
JFS
>> But the usual versions of functional programming are not higher-order
>> in the way logicians use the term. (022)
RM
> In what way, John? Are you challenging the validity of the
> Girard-Reynolds Isomorphism? (023)
No. It's an interesting theoretical result. I have a very high regard
for the current crop of functional programming languages, and I was
just observing that none of them depend in any way on the hierarchy
of infinite domains. (024)
RM
> While I'm writing a program, I'm quite un-naturally thinking in a
> syntactic sugar over the second order (polymorphic) lambda calculus.
>
> I am very unlikely to think about CL models. (025)
Since I can't observe your mental processes, I'll take your word
for what you think about. But I really doubt that there is anything
in any of your programs that could not be formalized in CL. (026)
RM
>>> to establish a hierarchy of types to avoid paradox. (027)
JFS
>> You don't need a hierarchy of types to avoid paradox. (028)
RM
> John, you are superimposing an inappropriate context on the statement
> I made to foist your polemic on me and others. (029)
I was stating a fact that Pat and Chris agreed with. (030)
What polemic are you talking about? The fact that I used the term
"kicking around" for a lot of the stuff published in the J. of Symbolic
Logic? I have spoken to logicians who agreed with me that many of
the things they published in their youth aren't very useful to what
they're doing in comp. sci. (031)
JFS
>> CL does not prevent you from using types. (032)
RM
> But CL is fully and completely type free and provides no semantics for
> types. (033)
The point I was making is that you can build a very wide range of type
systems within the CL framework. (034)
> Today, there are much more attractive alternatives in Martin-Lof type
> theory, constructive logics and univalent foundations. (035)
Fine. Are you using them in your current programming? (036)
I would venture to bet that any useful applications of those logics
could be implemented in versions that can be built on top of CL.
If you can find something useful that cannot be built on top
of CL that would indeed be worth a publication. (037)
JFS
>> In summary, you can map strongly typed logics to CL, if you want them.
>> If you really want to enforce the rules for strong typing, you can
>> even write a CL parser that would enforce those typing rules. (038)
RM
> This is absurd. Of course, unless you're paying. (039)
I meant that seriously. I don't know why you are objecting to. (040)
John (041)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (042)
|