Talk:Combinatory logic

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

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.

User:David Martland

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)

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)

Other title for this logic is Illative Combinatory Logic, briefly mentioned in Henk Barendregt Lambda Calculus as far as I remember. Addition to the article is done! — Preceding unsigned comment added by Elias (talk • contribs) 15:00, 30 March 2011 (UTC)

I reverted this change after reviewing appendix b of Barendregt Lambda Calculus. ILC is other Combinatory Logic, should be included either in other article or as a section in this one. — Preceding unsigned comment added by Elias (talk • contribs) 03:37, 31 March 2011 (UTC)

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:

1. T[V] => V
2. T[(E1 E2)] => (T[E1] T[E2])
3. T[λx.E] => (K E) (if x is not free in E)
4. T[λx.x] => I
5. T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)
6. T[λx.(E1 E2)] => (S T[λx.E1] T[λx.E2]) (if x is free in both E1 and E2)
7. T[λx.(E1 E2)] => (B T[λx.E1] T[E2]) (if x is free in E1 but not E2)
8. 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)

Rule 5 (T[λx.λy.E] => T[λx.T[λy.E]] (if x is free in E)) is mere hand waving. λx.T[λy.E] is not a correctly formed lambda-expression because T[λy.E] is in fact a SKI term.

Someone should check a copy of Barendregt out of the library and lay this thing to rest once and for all. It's also given in Field and Harrison (ISBN 0201192497), and probably a zillion other places. —Dominus (talk) 02:03, 22 August 2009 (UTC)

The transformation was published in Turner, D.A. (1979). "A New Implementation Technique for Applicative Languages". Software - Practice and Experience 9: 31, I will take a look on it.

As far as I remember the notation $\lambda ^{T}$, for the Turner abstractor is used in more recent papers in his honour. I can't remember one example at this moment.

There are also other transformations more efficient than Turner's where an ad-hoc basis is chosen according to each program, maybe by Hughes.

I can do this change after reviewing those papers, maybe another wikipedist have those articles at hand and can do this before I. — Preceding unsigned comment added by Elias (talk • contribs) 15:50, 30 March 2011 (UTC)

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)

(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)

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)

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

Λ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

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 (format changed by me to make the definitions more readable -- UKoch (talk) 19:18, 5 October 2012 (UTC))

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)

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)

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)

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)

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)

I would say it's worse than that. The long detailed section about lambda calculus appears *before* the detailed explanation of combinatory logic itself. It is a very distracting and confusing diversion from the main topic. If that section needs to be here at all, it should be at the end. But I agree with others who say that it should *not* be here, and should instead be replaced by a reference to the article about lambda calculus. StormWillLaugh (talk) 10:58, 17 June 2014 (UTC)

The part starting with "The expression E[v := a] represents..." and considering the next paragraph starting "By convention...": regarding this and the following paragraphs I don't understand what is being presented. I am not clear how these issues are related, although I can see it looks a bit LISP-ish. Jazzbox (talk) 00:46, 5 October 2010 (UTC)

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)

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:

1. (P ABSURDUM) = FALSE or
   
2. (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.

Or have I missed something important? -- Dominus (talk) 15:00, 13 December 2007 (UTC)

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)

I submitted the original version of the proof of undecidability. I am sure this or an equivalent proof can be found in generally accepted sources. Nowadays, Wikipedia wants verification. Does somebody know an acceptable reference to be added to the proof? Jos.koot (talk) 17:37, 13 June 2014 (UTC)

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)

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)

oppose Too much information specific to both articles. Potatoswatter (talk) 05:14, 11 March 2010 (UTC)

oppose' The topics are related, but they have too much unique information and each deserves an article Joaogcosta 22:12, 21 June 2010 (UTC) —Preceding unsigned comment added by Joaogcosta (talk • contribs)

Example of conversion to the S-K basis seems to be incorrect

Here, in Combinatory logic#Conversion of a lambda term to an equivalent combinatorial term, the correct conversion seems to be

T[λx.λy.(y x)]

= T[λx.T[λy.(y x)]] (by 5)

= T[λx.(S T[λy.y] T[λy.x])] (by 6)

= T[λx.(S I T[λy.x])] (by 4)

= T[λx.(S I (K x))] (by 3 and 1)

= (S T[λx.(S I)] T[λx.(K x)]) (by 6)

= (S (S T[λx.S] T[λx.I]) T[λx.(K x)]) (by 6)

= (S (S (K S) (K I)) T[λx.(K x)]) (by 3 twice)

= (S (S (K S) (K I)) (S T[λx.K] T[λx.x])) (by 6)

= (S (S (K S) (K I)) (S (K K) T[λx.x])) (by 3)

= (S (S (K S) (K I)) (S (K K) I)) (by 4)

The application in this case should look like

(S (S (K S) (K I)) (S (K K) I) x y)

= (S (K S) (K I) x (S (K K) I x) y)

= (K S x (K I x) (S (K K) I x) y)

= (S (K I x) (S (K K) I x) y)

= (K I x y (S (K K) I x y))

= (I y (S (K K) I x y))

= (y (S (K K) I x y))

= (y (K K x (I x) y))

= (y (K (I x) y))

= (y (I x))

= (y x)

Current example -- (S (K (S I)) (S (K K) I)) -- reduces to (y x) as well, but it couldn't be constructed by applying the six rules literally.

Am I right? Ximaera (talk) 10:00, 3 August 2008 (UTC)

No. Notice that the conversion rules are nondeterministic, there is more than one possibility how to construct a combinatorial term using the rules. In this particular example, it is possible express T[λx.(S I)] as (S T[λx.S] T[λx.I]) = (S (K S) (K I)) by rules 6 and 3 as you have done, but it is also possible to express it directly as (K (S I)) using just rule 3 as is done in the article. — Emil J. (formerly EJ) 10:47, 4 August 2008 (UTC)

Bolding in headings

Since headings are bold there is no reason to use bold in them. Why is the removal of redundant bolding causing problems for this page? Rich Farmbrough, 08:40, 8 September 2009 (UTC).

It's not redundant. It's clearly visible in browsers such as lynx, and it's semantically distinct. — Emil J. 10:41, 8 September 2009 (UTC)

Term Rewriting

I noticed that there is presently no connection to term rewriting systems at all. Should the definition of CL be formulated as a special form of TRS? —Preceding unsigned comment added by 83.85.21.120 (talk) 21:48, 7 February 2011 (UTC)

Bound variables vs Free variables

Near the beginning, it states

"Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions from which bound variables are absent."

However, this not only contradicts Haskel Curry's distinction between calculi and algebras ...

"The term 'algebra' is used in this book as a name for a system with free variables but no bound variables. Thus the system of Example 5 (Sec. 2C3) is an algebra and is aptly called propositional algebra. In contradistinction the term 'calculus' will, as a rule, be used to describe a system with bound variables, so that it is suitable to speak of a calculus of lambda conversion, a predicate calculus, etc. These terms agree with ordinary mathematical usage, where the distinguishing characteristic of the infinitesimal calculus, as opposed to elementary algebra, is the presence of bound variables in the former" -- "Foundations of Mathematical Logic" by Haskell B. Curry (sec. 4A1)

but also text in the definition later on:

"The primitive functions themselves are combinators, or functions that, when seen as lambda terms, contain no free variables."

I think the introductory text needs to be fixed. Free and bound variables can be confusing! — Preceding unsigned comment added by 99.190.134.97 (talk) 21:29, 2 February 2012 (UTC)

YES I agree, the sentence "Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions from which bound variables are absent." needs to be edited to read "Combinatory logic can be viewed as a variant of the lambda calculus, in which lambda expressions (representing functional abstraction) are replaced by a limited set of combinators, primitive functions with only bound variables" Can someone please add one more confirmation here, in which case I will go ahead and do the edit? — Preceding unsigned comment added by Davidleobonner (talk • contribs) 09:30, 10 January 2018 (UTC)

Technical Term

The technical term for what is called "Conversion of a lambda term to an equivalent combinatorial term" in this article is usually called "Bracket Abstraction". The name probably stems from the way the core part of the algorithm was intially written (my guess):

   [x]E = KE,  
   [x]x = I,  
   [x]Ex = E,  
   [x]EX = BE([x]X),  
   [x]XE = C([x]X)E,  
   [x]XY = S([x]X)([x]Y).

The above is Schönfinkel’s algorithm with Curry's combinators.

M. Schönfinkel.

Über die Bausteine der Mathematischen Logik.

Mathematische Annalen, 92:305–316, 1924.

Jan Burse (talk) 12:24, 4 December 2012 (UTC)

Are there still problems with the transformation T[ ]?

I have two problems with the definition of T[ ] as it is in this article:

1. With these rules you can't transform the expression \x.y as rule 3 requires that x is not free in y. Yet it is free according to the definition of free and bound variables in Lambda calculus#Free and bound variables. This would also mean that at least transformation 4 in the example is incorrect.

2. T[ ] is a function from lambda expressions to combinatory expressions. This means that in rule 5, a combinatory expression is applied to a lambda, which then has to be transformed again into combinatory. This makes no sense, you can't mix combinatory and lambda expressions that way.

I hope I am correct and someone will clarify this. --SemperVinco (talk) 06:28, 22 May 2014 (UTC)

Oops, never mind, rule 3 is correct. Still, rule 5 is weird. SemperVinco (talk) 08:46, 25 May 2014 (UTC)

incorrect italics, etc.

I fixed quite a few incorrect italicizations in E₁, changing it to E₁, and similarly with the subscript 2. Is there a reason why that notation was used, rather than E₁ and E₂? Michael Hardy (talk) 00:00, 27 July 2014 (UTC)

Is variable a combinatory term?

Combinatory logic is a notation to eliminate the need for variables in mathematical logic.

A combinatory term has one of the following forms:

• x
• P
• (E₁ E₂)

where x is a variable, ...

If there are should be no variables then why combinatory term can be a variable? — Preceding unsigned comment added by 95.106.255.17 (talk) 12:16, 6 August 2014 (UTC)

I fixed the introductory sentence: it's quantification and binding that is eliminated. ComputScientist (talk) 15:13, 6 August 2014 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Combinatory logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf to http://tromp.github.io/cl/LC.pdf

When you have finished reviewing my changes, please set the checked parameter below to true or failed to let others know (documentation at {{Sourcecheck}}).

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 12:05, 28 November 2016 (UTC)

External links modified

Hello fellow Wikipedians,

I have just modified one external link on Combinatory logic. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Added archive https://web.archive.org/web/20081029051502/http://cstein.kings.cam.ac.uk/~chris/combinators.html to http://cstein.kings.cam.ac.uk/~chris/combinators.html

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 04:19, 11 August 2017 (UTC)