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

learn more… | top users | synonyms

2
votes
1answer
142 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 ...
3
votes
1answer
131 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 ...
1
vote
1answer
67 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?
7
votes
0answers
127 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 ...
4
votes
1answer
136 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 ...
0
votes
0answers
53 views

Is the number of reduction orders a computable function?

Let $e$ be any expression in the SKI combinator calculus. Let $R(e)$ denote the number of possible reduction orders for $e$. Is $R$ a computable function? I believe that $R$ is not computable. But ...
3
votes
1answer
89 views

combinatory basis for head reduction

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 ...
0
votes
1answer
308 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 ...
7
votes
2answers
913 views

Can someone explain the Y Combinator?

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 ...
0
votes
2answers
708 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).