# Tagged Questions

Combinatory logic, combinatorial calculi, and other questions about combinators and variable-free variants of the $\lambda$-calculus.

10 views

### Combinatory logic - Evaluation exercise (abstraction and weak reduction)

I am going through the book "Lambda-Calculus and Combinators: An Introduction". I am trying to solve the following exercise: evaluation of $[x,y,z].xzy$ The result should be, according to solutions: ...
99 views

### What is the precise statement of Craig's theorem?

I'm interested writing a proof of Craig's theorem. After several attempts I realized that there are several possible ways to state the theorem, each with subtle but important differences. Here's one ...
29 views

### Can all computable numeric functions on church numerals in ski-combinator calculus be expressed using only completely evaluated terms?

Let a term in ski-combinator calculus be called "complete" if every primitive is partially applied (so all S's are applied to at most two arguments, all K's to at most 1, and all I's are not applied). ...
30 views

30 views

### Consistency of the SKI calculus as unprovability of S = K

The exercise I'm dealing with asks me to show that by adding $S = K$ to the usual reduction rules for the SKI-calculus, one obtains an inconsistent equivalence. This must be done without using Böhm's ...
55 views

### Hindley's “Introduction to combinatory logic”, exercise 6 chapter 2.

Can somebody help me with the following exercise? Find a combinator X such that X = S(KK)(XS). Reduction rules are usual: IX reduces to X (identity combinator) KXY reduces to X SXYZ reduces to XZ(...
42 views

### How to find the next higher combination out of a fixed group of digits?

I have a group of contiguous digits ordered from smallest to highest: 1234. I want a formula (in case it exists) to find the next closer higher combination of the same digits. In this example the next ...
28 views

### Proof of B, C, K, W system

There is a B,C,K,W system. In particular, there is presented the following identity: $B = S (K S) K$ How to prove this statement?
94 views

### Intuitively speaking, why was there a need to “eliminate” quantified variables in mathematical logic?

I'm trying to wrap my head around the understanding of lambda-calculus, from a math/computing/logic standpoint and am reading more about its very genesis. This has taken me to 1924 - Schonfinkel's ...
39 views

### On a corollary of the Church-Rosser Theorem

In the proof of Corollary 1.41.5 from Hindley-Seldin, $\lambda$-Calculus and Combinators - An Introduction, If $a$ and $b$ are atoms and $aM_1...M_m =_\beta bN_1...N_n$ then $a = b$ and $m = n$ ...
141 views

### In what sense is the S-combinator “substitution”?

According to the Wikipedia page on SKI-combinator calculus, I is the identity function, K is the constant function, and S is "substitution". I understand the first two, but I don't see what S has to ...
177 views

### Proof completion: if $Y$ is a closed term in strong nf, then $Yx$ weakly reduces to a strong nf $Z$

I am self-studying Hindley & Seldin's Lambda-Calculus and Combinators. I would appreciate some help with filling in a final detail for a proof for the following statement regarding combinatory ...
267 views

### Smullyan-To-Mock-a-Mockingbird, Find egocentric bird in L

Question (29, p. 81). Let me tell you the most surprising thing I know about larks: Suppose we are given that the forest contains a lark $L$ and we are not given any other information. From just this ...
316 views

### How to represent Smullyan's “Mockingbird” puzzles in (Homotopy) Type Theory?

(If you're unfamiliar with the puzzles from To Mock a Mockingbird, three pages tell you everything you should need.) Is it possible to solve the riddles in To Mock a Mockingbird in a "propositions as ...
89 views

### Why SKI when SK is complete

Why people talk about SKI calculus when S and K combinators can be used to create any other combinator including I?
176 views

### Where to go after _To Mock A Mockingbird_?

So long ago I read Raymond Smullyan's delightful To Mock A Mockingbird, a gentle introduction to combinatory logic (representing combinators as 'birds' singing back and forth to each other). I fell ...
168 views

### Prove that all combinators must fulfill A x = x for some x, given that M x = x x and composability of any two combinators

I'm working through Raymond Smullyan's "To Mock a Mockingbird" and I'm stuck on the first problem in the combinatory logic section. I'd appreciate hints, but no spoilers please. The problem is ...
920 views

### Proving a combinator is a fixed point

Show that the term ZZ where Z is λz.λx. x(z z x) satisfies the requirement for fixed point combinators that ZZM =β M(ZZM).
1k views

### Looping (ω) Combinator

Can someone explain this combinator? I understand $\lambda x. x$, but I don't understand $\lambda x. x x$ From what I've gathered, this means given x, return the application of x to x. I don't ...
The Y combinator is a concept in functional programming, borrowed from the lambda calculus. It is a fixed-point combinator. A fixed point combinator $G$ is a higher-order function (a functional, in ...
Consider combinatory calculi that don't have tail reduction. So there may be combinators $x$, $y$ and $z$ such that $y\to z$ but $xy\nrightarrow xz$. We can still write every combinator as a ...