Talk:Combinatory logic

From Wikipedia, the free encyclopedia

Could we put, right at the very beginning of the page, a definition of combinator -- since this is the page that we're taken to when we search for, or click on a link to, Combinator? Much later in the article, it appears that the definition is, "a function with no free variables." Is that correct? --Mike Schiraldi 3 July 2005 15:31 (UTC)

That is a good idea. However, my feeling is that a function with no free variables is not accurate enough even for introducing the subject. Unfortunately, I can't think of something better. Possibly, the introductory chapter of Curry's book (see the references in the article) may include a better definition. Koffieyahoo 5 July 2005 06:33 (UTC)

	Pending tasks for Combinatory logic :	edit this list - add to watchlist - purge
	Combinatory terms as graphs section Expand or merge B,C,K,W system page

An interesting start. I picked this up from the comment in Lambda calculus

Are you going to do supercombinators?

I had hoped that someone more familiar with compiler construction would complete that part of the 'Applications' section and discuss supercombinators in the process. (Dominus 20:04 Nov 23, 2002 (UTC))

Also, related topics might include graph reduction machines.

User:David Martland

Is this the same subject as what is called "combinatory" logic? "Combinatorial" usually means "pertaining to combinatorics"; is the same meaning intended here? -- Mike Hardy

The title is wrong: it should be "combinatory logic". See for instance http://catalog.loc.gov/cgi-bin/Pwebrecon.cgi?Search_Arg=combinatorial+logic&Search_Code=SUBJ_&PID=14368&CNT=25&BROWSE=21&HC=18&SID=1 . "Combinatorial logic" is often used for boolean logic used in circuit design. I am renaming. AxelBoldt 19:50 Nov 23, 2002 (UTC)

Thanks. Dominus 20:04 Nov 23, 2002 (UTC)

Possible error in Turner's T[ ] Transformation: In rules 7. and 8., terms E2 and E1 resp. remain untransformed. I think the correct rules are:

T[V] => V
T[(E1 E2)] => (T[E1] T[E2])
T[λx.E] => (K E) (if x is not free in E)
T[λx.x] => I
T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) (if x is free in both E1 and E2)
T[λx.(E1 E2)] => (B T[λx.E1] T[E2]) (if x is free in E1 but not E2)
T[λx.(E1 E2)] => (C T[E1] T[λx.E2]) (if x is free in E2 but not E1)

Does that look right? --Fritz Obermeyer

The role of C and B are reverted from the tradition which is 75 years old!!! 15 January 1929!, item A. Page 2 of 13.
Of course, David Turner never invented this, (nor pretend it, I think)
If authors dont correct it, I will do it after finishing traduction to spanish.

Thanks. DefLog 13:21, 25 Mar 2004 (UTC)

1 (K E) if x does not appear free in E
2 Multiple views of the Lamda calculus
3 Question about the substitution syntax
4 ΛK versus ΛI
5 numerals
6 B,C,K,W system

[edit] (K E) if x does not appear free in E

Wait a minute! Just being equivalent isn't enough -- there could still be lambdas in there! I changed the rule, but someone better than I should change the commentary.) 64.0.112.160

[edit] Multiple views of the Lamda calculus

There is a bad tendency for Wikipedia entries to take one view of something, and word things as if "that's the way it is". I fixed the wording to say that 'one' way to view it is as equivalent to the Lambda calculus, and give another view and a reference to support it. I, for reasons obvious to any who know me, chose a recent reference that has a good bibliography on some of it. (There are some notes in my websites modal logic axioms pages that cover part of this.)

However, this is still a bit incomplete... since it was in some reasonable sense a competitor of Lambda Calculus before the equivalence was proven. There were, at the time, many different (competing) models of computation.

The "combinators as logic" view is common in early papers discussing for which systems Merideth's condensed detachment is complete. (And the interesting result that the completeness of Condensed Detachment depends on the axioms one is using for the system, and not on which logic system you have. See, for example [[1]] or Hindley's book that is being reviewed there. )

The wikipedia pages are skimpy on any of the historical development... But give the recent rise of Condensed Detachment in current computer investigations of minimal axiom sets for systems, there really ought to be (in my opinion) a page on Condensed Detachment and on Crue Merideth. (See, for example, "New Elegant Axiomatizations of Some Sentential Logics " by Branden Fitelson (2001), [[2]] and the related pages)

-- User:Nahaj

I forgot I had this comment out here... Update: There is now a Condensed Detachment page. Nahaj 17:47, 16 January 2006 (UTC)

[edit] Question about the substitution syntax

Is the substitution syntax incorrect? I think "E[a/v]" should be "E[v/a]" ... i.e. the variable comes first.

The page currently shows:

(λv.E a) => E[a/v]

On the Lambda calculus page, the following syntax is used for substitution:

((λ V. E ) E' ) == E [V/E' ]

--Ingenuus 05:31, 5 Jun 2005 (UTC)

The usual reading of a construction like "E[a/v]" is: Substitute "a" for "v" in "E". Hence, since we are replacing the v's by a's the current notation is correct. It was wrong on the Lambda Calculus page. I changed it to the more readable: "E[v := a]" on both the Lambda Calculus page and the current page -- Koffieyahoo 14:04, 13 Jun 2005 (UTC)

The link of "Lectures on the Curry-Howard Isomorphism". Sørensen, Morten Heine B. and Pawel Urzyczyn is broken. The Lectures can be found at http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf -- User:Mpagano

[edit] ΛK versus ΛI

The presentation of the combinators B and C do not clarify why they should be introduced once we have already combinator K. The issue is the difference between the ΛK and the ΛI-calculus. ΛI delimits abstractions λx.M to forms in which x occurs free in M. K==λx.λy.x does not belong to ΛI. B and C do belong to ΛI and locally act as K. See Barendrecht chapter 9. User: Jos.koot

[edit] numerals

The most straight forward representation of natural numbers is not mentioned: zero == identity add1 == (λx.λz.zFx) zero? == (λx.xT) sub1 == (λx.xF) user:Jos.koot

added: In fact every non trivial question is undecidable, or more precisely: there is no complete non trivial predicate. A predicate is a combinator that, when applied, either returns T or F. A predicate N is non trivial if there are two combinators A and B such that NA=T and NB=F. A combinator N is complete if and only if NM has a normal form for every combinator M. Allong the same lines as above it can be proven (by reductio ad absurdum) that no complete non trivial predicate exists. Jos.koot 11:13, 25 August 2006 (UTC)Jos.koot