Combinator logic and types

[Russell Wallace]

In lambda calculus, the meaning of a term depends on its enclosing
context. The biggest attraction of translating into CL is that it
would render terms context free - or put another way, it would give
terms value semantics.

But arguably this is only true in the untyped version. Even in CL, the
type of a term still depends on context. And type is part of the
meaning, it affects what inferences we are licensed to perform. (And
even if we ultimately want to regard types as predicates, we still
need to bootstrap the whole system on a bottom layer type system of
the usual variety, to avoid paradoxes by determining what constitutes
a valid predicate.)

Does this mean that typed CL terms aren't going to have value
semantics after all, and therefore we might as well stick with lambda
and avoid paying the various costs of translation into CL?

[Russell Wallace]

More specifically, consider (whether in CL or lambda) the function =,
whose type is a -> a -> boolean, for any type a. The type inference
algorithm has the job of filling in the specific value of a wherever
possible. (Why? Because one of the jobs of the type system is to guard
against non-termination paradoxes, but another is to license
inferences. If we see a term like x=false, we need to be able to
propagate the type information across the = to deduce that x is of
type Boolean, which in turn enables us to conclude that regardless of
whether x is false, we know it must always be either true or false.)

This in turn would seem to mean (somebody please correct me if I'm
missing something) that = can't be a single object, but must be a
class of objects, one instance per occurrence, so that each occurrence
may be filled in with a different specific type.

[Abram Demski]

Russel,

It sounds like you are leaning towards using typed logic. As you say, this is not really a problem if the underlying logic is untyped. I'd think the idea might be to have a typed logic at the user level, but have an underlying untyped logic which it gets interpreted into. Type-reasoning will be important, since it is a heavily developed way of certifying propositions as meaningful, but at the same time it will be just another automated inference algorithm within the system.

For this to work, we need to find an untyped logic which supports talking about types in a manner very close to the standard.

--Abram

--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

--
Abram Demski
http://lo-tho.blogspot.com/
http://groups.google.com/group/one-logic

[Russell Wallace]

Yes, that's basically the lines I'm thinking along - we would like the
ultimate semantics to be untyped, but we have to make use of types at
least at the basic level.

Here's a thought I just came up with. The reason types are such a big
headache is basically because they have to be carried around, they
gunk up the _data_.

Suppose we store all terms as untyped, but every time we make an
inference, on the spot we run the usual type inference algorithm on
the newly generated term, and reject it if it doesn't pass. That way
whatever complexity there may be can be incorporated into a single
_procedure_, which is vastly more benign.

(Also, if we want to allow more sophisticated ways of proving
termination later, they could be added to that procedure.)

Is it okay to do this? Can type information be thus localized in space and time?

That would cover the role of types in safeguarding against paradox.
There is also their role in licensing inference.

But the safeguarding was the hard part. The reason is because you
can't start making types be predicates, at least not by itself, you
can't just have Halts(T) as a predicate, or you just run into
strengthened versions of the paradoxes.

The role of types in licensing inference, however, might perhaps not
have that property, and might be covered by making types be normal
predicates?

[Russell Wallace]

> Is it okay to do this? Can type information be thus localized in space and time?

As far as I can see, the answer is yes, that is, when the question we
are asking is "can this term be consistently assigned some finite type
(we don't care exactly what)", then we can answer it just by running
the usual type inference algorithm on the term in isolation. I think
doing this with every inferred statement should be sufficient to
safeguard against paradox. Someone please correct me if I'm wrong.

[Russell Wallace]

There is then the question of how we capture, for inference purposes,
the information types provide.

Among the things we want to be able to figure out are,

Suppose we have an occurrence of x!=false somewhere in the input
(assuming the input is in the form of typed lambda calculus)

deduce x:bool

Translate that into bool(x)

And the system should already know:
bool(x) = (x=true | x=false)

from which it should be possible to deduce x!=false => x=true

similarly, if x has been used in an integer context, we can figure out int(x)

What about functions? Suppose + is the addition function on integers,
how do we represent this? I suppose something like
int(X) & int(Y) <=> int(X+Y)

In TPTP format, + is polymorphic over the various numeric types
perhaps we could represent this as
int(X) & int(Y) <=> int(X+Y)
rat(X) & rat(Y) <=> rat(X+Y)
real(X) & real(Y) <=> real(X+Y)

though of course it would be nicer if we could represent it as
type(X+Y) = type(X) = type(Y)

How do we define type so as to make this possible? It can't be just
any predicate, because the above is true for type=int, but not for
type=even.

Does the definition of type have to make a list of known basic types,
and how to compose them into compound types?

[Abram Demski]

Russel,

Sorry for the slow reply! I think these questions need to be answered in view of a specific logic. Have you looked at the systems in Cantini yet? Or any others?

--Abram

--
You received this message because you are subscribed to the Google Groups "One Logic" group.
To post to this group, send email to one-...@googlegroups.com.
To unsubscribe from this group, send email to one-logic+...@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/one-logic?hl=en.

[Russell Wallace]

Okay, for the sake of definiteness lets say our reference logic system
is HOL Light; it seems to be perhaps the most accessible one.