good book on combinatory logic

11 views
Skip to first unread message

translogi

unread,
Dec 8, 2007, 7:42:19 AM12/8/07
to
Does anybody know a simple book on combinatory logic?

I read Smullyans "how to mock a mockingbird" is interesting but is a
bit to much about combinators and not a lot about where it is good for
or how you can use it.

Or is the subject matter just to difficult for an simple book?

Am primarily interested how to "simulate" First order logic (predicate
logic with relations / FOL) in this logic.

(smullyan at the end of his book goes into arithmetic but i am loking
for FOL)

Thanks

Jack Campin - bogus address

unread,
Dec 8, 2007, 8:28:36 PM12/8/07
to
> Does anybody know a simple book on combinatory logic?
>
> I read Smullyans "how to mock a mockingbird" is interesting but is a
> bit to much about combinators and not a lot about where it is good for
> or how you can use it.
>
> Or is the subject matter just to difficult for an simple book?

Hindley and Seldin, Introduction to Combinators and {\lambda}-calculus,
Cambridge 1986.

> Am primarily interested how to "simulate" First order logic (predicate
> logic with relations / FOL) in this logic.

You can't.

============== j-c ====== @ ====== purr . demon . co . uk ==============
Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760
<http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975
stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557

translogi

unread,
Dec 9, 2007, 7:39:06 AM12/9/07
to
On Dec 9, 1:28 am, Jack Campin - bogus address

<bo...@purr.demon.co.uk> wrote:
> > Does anybody know a simple book on combinatory logic?
>
> > I read Smullyans "how to mock a mockingbird" is interesting but is a
> > bit to much about combinators and not a lot about where it is good for
> > or how you can use it.
>
> > Or is the subject matter just to difficult for an simple book?
>
> Hindley and Seldin, Introduction to Combinators and {\lambda}-calculus,
> Cambridge 1986.

thanks will have a look to that


>
> > Am primarily interested how to "simulate" First order logic (predicate
> > logic with relations / FOL) in this logic.
>
> You can't.
>

I thought if it is strong enough for arithmetic it must be strong
enough for Fol.

or is it only strong enough for nomadic Fol (for without relations)
this is a bit ruining my plans.

Can you elaborate a bit on this?

Jan Burse

unread,
Dec 9, 2007, 9:48:01 AM12/9/07
to
Jack Campin - bogus address schrieb:

>> Does anybody know a simple book on combinatory logic?
>>
>> I read Smullyans "how to mock a mockingbird" is interesting but is a
>> bit to much about combinators and not a lot about where it is good for
>> or how you can use it.
>>
>> Or is the subject matter just to difficult for an simple book?
>
> Hindley and Seldin, Introduction to Combinators and {\lambda}-calculus,
> Cambridge 1986.
>
>> Am primarily interested how to "simulate" First order logic (predicate
>> logic with relations / FOL) in this logic.
>
> You can't.

Strictly speaking I would confirm, you can't.

But because combinatory logic corresponds to propositional
hilbert style proofs with some axioms (Watch out this
is not the usual curry howard isomorphism which is between
typed lambda calculus and intuitionistic logic. We
are not dealing with typed lambda calculus here, but
with untyped combinatory logic).

And because choosing the right axioms, and thus the
right combinators, yields classical logic. I would
say combinatory logic yields at least propositional
logic. The question is now how we could make the step
to predicate logic, that is replace propositional
variables by prime formulas, and allow quantifiers.

What FOL rules would you like to give a combinatorial
term? If you tell us what FOL rules you are interested
in, then maybe we can give you further hints. Will
you stick to hilbert style proofs?

Best Regards

translogi

unread,
Dec 9, 2007, 1:40:31 PM12/9/07
to

Thanks it is allready getting to complicated for me here.

In Smullyans book i read that you can do arithmetic in Combinatory
logic
In schonfinkel;s article that you could do first order logic in it
(article in from frege to Godel) the article does not go beyond
nomadic FOL.
found a reference to an article from Quine about it (but havent read
that one yet)

that is about how far i am.

don't have the faintest idea what you mean by:
curry howard isomorphism
typed lambda calculus
untyped combinatory logic

am also not good in Hilbert style proofs

Think i must look for another subject for an essay.

I was thinking that you just could replace FOL with Combinatory logic
to get rid of the distibnction between variables and predicates. and
only have combinators.

thanks anyway

translogi

unread,
Dec 15, 2007, 7:39:17 PM12/15/07
to
> thanks anyway- Hide quoted text -
>
> - Show quoted text -

Did read

Variables Explained Away
Willard V. Quine
Proceedings of the American Philosophical Society, Vol. 104, No. 3.
(Jun. 15, 1960), pp. 343-347.

And that does "full" FOL in combinatory logic. (First order Logic
including relations)

But it is hopelessly complicated.
and i am wondering about his major inversion Inv combinator.


Jan Burse

unread,
Dec 16, 2007, 6:21:18 AM12/16/07
to
translogi schrieb:

> On Dec 9, 6:40 pm, translogi <wilem...@googlemail.com> wrote:
>> On Dec 9, 2:48 pm, Jan Burse <janbu...@fastmail.fm> wrote:
>>> The question is now how we could make the step
>>> to predicate logic, that is replace propositional
>>> variables by prime formulas, and allow quantifiers.
>>> What FOL rules would you like to give a combinatorial
>>> term? If you tell us what FOL rules you are interested
>>> in, then maybe we can give you further hints. Will
>>> you stick to hilbert style proofs?
>>> Best Regards
>> Thanks it is allready getting to complicated for me here.
>>
>> don't have the faintest idea what you mean by:
>> curry howard isomorphism
>> typed lambda calculus
>> untyped combinatory logic
>> am also not good in Hilbert style proofs
> Did read
>
> Variables Explained Away
> Willard V. Quine
> Proceedings of the American Philosophical Society, Vol. 104, No. 3.
> (Jun. 15, 1960), pp. 343-347.
> And that does "full" FOL in combinatory logic. (First order Logic
> including relations)
> But it is hopelessly complicated.
> and i am wondering about his major inversion Inv combinator.

This one?
http://www3.unifi.it/dpfilo/upload/sub/Didattica/Minari/varexplaw.pdf

This reminds of the "unpacking the axiom scheme of class
comprehension" for NBG.
http://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2%80%93G%C3%B6del_set_theory#Unpacking_the_axiom_scheme_of_Class_Comprehension

Not sure whether one arrives at a *proof theory* for
FOL, but rather only (sic!) variable less *formulas* for FOL
and set theory.

Crucial to have variable less formulas for FOL is to
have a projection operator. An operator that sends
"A(x,y)" to "exists x A(x,y)".

You might like the following paper (see page 8):
http://www.iam.unibe.ch/til/publications/submitted
G. Jäger: Operations, sets and classes
E(f) = t <-> exists x(fx = t).

I am still confident that one can develop combinatorials
for proofs of FOL, and this is what is more in the focus
of my interest. Think this runs under the heading of *calculus
of construction*, but I didn't find a reference right now.
Maybe can provide you one in a next post.

Combinatorials for proofs will also turn the prime
formulas into variable less formulas, and that is what
I see manifest in the papers above. Maybe its better
to direct this process in a special way by the quine/
bernays/jaeger approaches for set theory, instead of
having a general FOL approach and then stepping into
set theory.

I am not so sure about the advantages and disadvantages.

Best Regards


Jan Burse

unread,
Dec 16, 2007, 3:43:12 PM12/16/07
to translogi
translogi schrieb:

> Did read
>
> Variables Explained Away
> Willard V. Quine
> Proceedings of the American Philosophical Society, Vol. 104, No. 3.
> (Jun. 15, 1960), pp. 343-347.
>
> And that does "full" FOL in combinatory logic. (First order Logic
> including relations)
>
> But it is hopelessly complicated.
> and i am wondering about his major inversion Inv combinator.

If you do not involve set theory and when you are
not interested in a proof theory, but only
expressing formulas without variables. Then you
can go along as follows:

The SKI conversion needs only be applied
to expressions of the form lambda x.t.

Prime formulas do not have this form, so they
stay as they are. Although they might include
variables. These variables are later removed,
when they are bound by quantifiers. The function
symbols in the prime formulas are simply treated
as new combinatorial constants and the variables
as variables.

Example:

p(f(x),y) corresponds to (p (f x) y)


What remains are formulas which have the prime
formulas in their leafs and conjunctions and
quantifiers in the nodes. We should fix a set
of junctions and quantifiers we would like
to work with. Lets assume we restrict ourselfs
to the following:

~: negation
&: Conjunction
exists x: Existential Quantification

Now we introduce combinatorial constants for
our set of junctions and quantifiers:

~A := (NEG A)
A & B := (AND A B)
exists x A := (EXISTS (lambda x.A))

The existential quatifier introduces a lambda
abstraction which can be removed via the
SKI combinatorials, which will also remove the
x inside the quantified formula A.

Example:

forall y(q(y) -> p(y))

==

~exists y(q(y) & ~p(y))

==

(NEG (EXISTS (lambda y (AND (Q y) (NEG (P y))))))

== (*)

(NEG (EXISTS (S (S (K AND) (S (K Q) I)) (S (K NEG) (S (K P) I)))))

== (**)

(NEG (EXISTS (S ((B AND) Q) ((B NEG) P))))


Best Regards

(*)
http://cs.wwc.edu/~aabyan/LN/PL/book/node108.html#lc:ski
http://en.wikipedia.org/wiki/Combinatory_logic#Completeness_of_the_S-K_basis
(**)
http://cs.wwc.edu/~aabyan/LN/PL/book/node109.html#ski:optim
http://en.wikipedia.org/wiki/Combinatory_logic#Combinators_B.2C_C

Reply all
Reply to author
Forward
0 new messages