Talk:Combinatory logic
From Wikipedia, the free encyclopedia
 |
|||||
| Mathematics rating: | B Class | Mid Priority | Field: Foundations, logic, and set theory | ||
| Please update this rating as the article progresses, or if the rating is inaccurate. Please also add comments to suggest improvements to the article. | |||||
[edit] Definition of combinators
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)
An interesting start. I picked this up from the comment in Lambda calculus
[edit] Supercombinators
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.
[edit] About combinatorics
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
It is not about combinatorics. Combinators just combine together more terms, that's the reason of this name. --Blaisorblade (talk) 14:24, 6 January 2008 (UTC)
[edit] Wrong title
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)
[edit] Wrong definition of T[ ] ?
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 definition of Turner's T in today's revision seems correct (i.e. as above and with an extra T in clause 3) Hugo Herbelin (talk) 15:46, 23 December 2007 (UTC)
- I have still a few questions about the transformations T:
- - Is there any reason why it is not split into two parts: a part for abstraction elimination in a pure expression of combinatory logic (as it seems it is most standardly done - I saw this e.g. in the paper "A ‘new’ abstraction algorithm" by Price and Simmons), and a part for iterating abstraction elimination so that to convert a lambda terms into a term of combinatory logic? If the transformation were so-split into two parts, one could then say that the pure abstraction elimination part is in Curry-Howard correspondence with the deduction theorem of Hilbert-style logic, which is an interesting observation in itself (see Deduction_theorem#Conversion from proof using the deduction meta-theorem to axiomatic proof).
- - In the main (non Turner's) translation, is there any reason why the 3rd clause is not replaced by the simplest clause T[λx.y] => K y, and, in the same time, the condition on freshness of x in the 5th clause removed? I guess that this is a way to optimize the size of the resulting term but if it is the reason for, it would be worth to tell it. Otherwise, the reader may wonder why the alternative proposition that more canonically works by simple case analysis on the different possible forms of a term is not used. Hugo Herbelin (talk) 15:46, 23 December 2007 (UTC)
[edit] Swapped C and B
- 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)
[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
- 64.0.112.160 fixed the definition of T[ ]. I applied the same correction in section "Explanation of the T[ ] transformation". Hugo Herbelin (talk) 13:21, 23 December 2007 (UTC)
[edit] Multiple views of the Lambda 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
This is a typical result in computability theory, where it is called Rice's theorem. An important conceptual point is that it is about predicates on the chosen representation of computable functions (be it a Turing machine, a lambda term or a term of combinatory logic), and it descends from the Halting problem.
--Blaisorblade (talk) 14:13, 6 January 2008 (UTC)
[edit] B,C,K,W system
The article on the B,C,K,W system was in an awful state. I cut out some stuff, but now it is rather short. Leibniz 21:40, 10 November 2006 (UTC)
[edit] Lazy K is "purer" than Unlambda
The article asserts:
- The purest form of this view is the programming language Unlambda, whose sole primitives are the S and K combinators and character IO.
This is no longer the case. Lazy K eliminates the I/O primitives by making the "lazy stream" technique mandatory (i.e. a program is just a function on infinite lists of natural numbers). So it is purer. Unfortunately the article Lazy K doesn't exist yet, so I'm not going to change the link just yet. Hairy Dude 03:48, 5 January 2007 (UTC)
- IIRC Lazy K was AfD'd half a year ago, along with a host of other esoteric languages. -- EJ 11:02, 5 January 2007 (UTC)
[edit] The X combinator
I am grateful to the author(s) of the section on the reduction of the {S,K} basis to the minimalist basis {X}, as that is a confused subject in Curry et al (1972), Barendregt (1984), and Wolfram (2003). I wish someone would devise an elegant axiom set in terms of X alone.
BTW, as best as I can determine, Wikipedia regrettably has no entry on Quine's predicate functors. 202.36.179.65 18:21, 2 March 2007 (UTC)
[edit] Why is there a section on lambda calculus?
The section on the lambda calculus is one of the biggest sections in the page - this doesn't seem quite right. What is says is fine, but I don't think it belongs here.
cheers, Tom Conway
- I agree, lambda calculus has it own page and the contents of the section on lambda calculus in the combinatory logic page which is not already present in the lambda calculus page would better move there.
- Lambda calculus is of course relevant for comparison with combinatory logic but the section Combinatory logic in computing already mentions lambda calculus and already highlights the connection with combinatory logic, which looks enough for a smooth reading of section Combinatory calculi.
- Lambda calculus is largely referred to in section Completeness of the S-K basis. Not so much for defining abstraction elimination (which could be done internally to combinatory logic, as it it done in Barendregt, chapter 7), but for stating that CL and lambda calculus have a similar expressivity (in fact the same expressivity if extensionality is added). I believe that with a slight reworking in the way the S-K section is presented, an external reference to the lambda calculus page would suffice.
- I have a side question: does anyone know where does the terminology combinatory calculus (used in the article) come from? Is it a strict synonym of combinatory logic with a more computational flavor or does it denote a different approach of combinatory logic (e.g. based on a notion of reduction rather than on a notion of equational reasoning)? In any case, it would certainly be good to give a short explanation in the article of why the two terminologies are used. Hugo Herbelin (talk) 14:27, 23 December 2007 (UTC)
[edit] One point basis
I added X' ≡ λx.(x K S K) as an example of a one point basis in CL without extensionality. Jos.koot (talk) 21:22, 12 December 2007 (UTC)
[edit] Undecidability
A predicate is a combinator, say P such that for every combinator A either
(P A) = FALSE or
(P A) = TRUE or
(P A) has no normal form.
A predicate P is complete if (P A) has a normal form (either FALSE or TRUE) for every A.
A predicate P is non trivial if there are combinators F and T such that
(P F) = FALSE and
(P T) = TRUE.
Theorem: there is no complete non trivial predicate
Proof By reductio ad absurdum. Suppose there is a complete non trivial predicate, say P.
Because P is supposed to be non trivial there are a T and an F such that
(P T) = TRUE and
(P F) = FALSE.
Define NEGATION ≡ λx.(if (P x) then F else T) ≡ λx.((P x) F T)
Define ABSURDUM ≡ (Y NEGATION)
Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM).
Because P is supposed to be complete either:
- (P ABSURDUM) = FALSE or
- (P ABSURDUM) = TRUE
Case 1: FALSE = (P ABSURDUM) = P (NEGATION ABSURDUM) = (P T) = TRUE, a contradiction.
Case 2: TRUE = (P ABSURDUM) = P (NEGATION ABSURDUM) = (P F) = FALSE, again a contradiction.
Hence (P ABSURDUM) is neither TRUE nor FALSE, which contradicts the presupposition that P would be a complete predicate. QED.
From this undecidability theorem it immediately follows that there is no complete predicate that can disciminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is no complete predicate, say EQUAL, such that:
(EQUAL A B) = TRUE if A = B and
(EQUAL A B) = FALSE if A ≠ B.
If EQUAL would exist, then for all A, λx.(EQUAL x A) would have to be a complete non trivial predicate.
This may require some more editing, but would it be a good idea to include this proof in the article? Jos.koot (talk) 23:16, 12 December 2007 (UTC)
- I don't understand this:
-
- A predicate P is non trivial if there are combinators F and T such that PF = F and PT = T.
- It seems to me that you are using F and T in two different ways here. You have already said that a combinator P is a predicate if Px = F or T whenever Px has a normal form. This is enough to define F and T in terms of P. You can't then require that PF = F.
- I think what you want to say is that a predicate P is nontrivial if there are combinators f and t such that Pf = F and Pt = T.
- Oh, I see now. You are distinguishing between F and F. I did not notice this on the first reading. I suggest that if you put this proof into the article, you rely on something other than the typeface to distinguish these. Maybe use TRUE and FALSE in place of T and F. -- Dominus (talk) 15:01, 13 December 2007 (UTC)
Yes, I made the distinction between F and F. I edited this section accoding to your suggestion. Let me know what you think of it, please. Jos.koot (talk) 09:39, 14 December 2007 (UTC)
On second thought, I decided to use the same terminolgy as already used in the section on undecidability Jos.koot (talk) 12:57, 14 December 2007 (UTC)
[edit] Metadiscussion: encapsulating isolated discussion topics into proper sections?
Would not it be preferable to move the discussion topics that are not in a proper section (i.e. those coming before the table of contents) within sections. I think it would make the discussion page clearer as all discussed topic would then be on the same level)? Hugo Herbelin (talk) 14:35, 23 December 2007 (UTC)
Done. I indeed felt this page messy upon viewing it, for this exact reason. --Blaisorblade (talk) 14:24, 6 January 2008 (UTC)
[edit] Merger proposal
SKI combinator calculus talks about the same exact topic of this page; however, the treatment is really different, but I do not think they should be separate pages. The merge however is nontrivial, and I do not think I would be able (if the merge is accepted) to do it by myself. Any opinion?
--Blaisorblade (talk) 14:17, 6 January 2008 (UTC)
- A merge would be much natural since the SKI calculus is a particular instance of combinatory logic. A preliminary step could be to say more clearly in the lead section that SKI is a complete system of combinators for combinatory logic, where the combinator I, which is redundant, is included in order to shorten a bit the size of expressions. --Hugo Herbelin (talk) 18:30, 6 January 2008 (UTC)
- A merge doesn't make sense because the presnt article on combinatory logic is already too long. The article on combinatory logic should probably be broken down into a number of separate articles. A B Carter (talk) 21:59, 14 May 2008 (UTC)
