[Propositions As Types] - A New Kind of Science: The NKS Forum

A New Kind of Science: The NKS Forum

Pages:1


Propositions As Types

(Click here to view the original thread with full colors/images)


Posted by: Jon Awbrey

PAT. Note B1

I think it's best to begin with a few simple observations,
as I frequently find it necessary to return to the basics
again and again, even if I take a different path each time.

Observation 1

We can abbreviate this inference, that operates on
two pieces of information to produce another piece
of information, in the following conventional form:

In this scheme of inference, the notations "x", "f", and "f(x)"
are taken to be names of formal objects. Some people will call
these notations by the name of "terms", while other people will
somewhat more confusedly say that the formal objects themselves
are the terms. Because it is so important to distinguish signs
denoting from objects denoted, I will make some effort to avoid
the latter usage, and recommend sticking with the first option.

In the same context, the notations "X", "X -> Y", and "Y" give us
information, or indicate formal constraints, that we may think of
as denoting the "types" of the formal objects under consideration.
By an act of "hypostatic abstraction", one may of course elect to
view these types as a species of formal objects existing in their
own right, inhabiting their own niche, as it were.

If a moment's spell of double vision leads us to see the
functional arrow "->" as the logical arrow "=>", then we
may observe that the right side of this inference scheme
follows the pattern of logical deduction that is usually
called "modus ponens". And so we forge a tentative link
between the pattern of information conversion implicated
in functional application and the pattern of information
conversion involved in the logical rule of modus ponens.

Jon Awbrey


Posted by: Jon Awbrey

PAT. Note B2

I'm working from a sheaf of notes that I wrote out
seven or eight years ago, and what with travel and
vacation and all it looks like it will take the rest
of the summer to come up with a coherent exposition,
but people who are already familiar with the subject
and want to look at it from what I think are a couple
of new angles could peruse the thread that begins here:

PAT A. http://stderr.org/pipermail/inquiry...hread.html#1643
PAT A. http://stderr.org/pipermail/inquiry...hread.html#1677

Notice that I am carrying out combinator applications "on the right",
so the formulas may be backwards from what many people are used to.

Jon Awbrey


Posted by: Jon Awbrey

PAT. Note B3

Here are a couple of references that are especially
pertinent to the use of combinators in computation:

| Lambek, J. and Scott, P.J.,
|'Introduction To Higher Order Categorical Logic',
| Cambridge University Press, Cambridge, UK, 1986.
| http://titles.cambridge.org/catalog...isbn=0521356539

| Smullyan, R.,
|'To Mock a Mockingbird, And Other Logic Puzzles,
| Including an Amazing Adventure in Combinatory Logic',
| Alfred A. Knopf, New York, NY, 1985.

Jon Awbrey


Posted by: Jon Awbrey

PAT. Note B4

Another good reference on combinatory logic and lambda calculus,
intermediate in level between the previous two that I mentioned:

| J. Roger Hindley & Jonathan P. Seldin,
|'Introduction to Combinators and [Lambda]-Calculus',
| London Mathematical Society Student Texts #1,
| Cambridge University Press, Cambridge, UK, 1986.

Jon Awbrey




Forum Sponsored by Wolfram Research

© 2004-2010 Wolfram Research, Inc. | Powered by vBulletin 2.3.0 © 2000-2002 Jelsoft Enterprises, Ltd. | Disclaimer
vB Easy Archive Final - Created by Xenon and modified/released by SkuZZy from the Job Openings