Skip to main content

Questions tagged [combinatory-logic]

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

Filter by
Sorted by
Tagged with
3 votes
2 answers
80 views

Defining the Y combinator in terms of S, K and I

We know that the Y-combinator is defined as: $$\text{Y}:=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))$$ Wikipedia says :$$\text{Y}:=\text{S(K(SII))(S(S(KS)K)(K(SII)))}$$ Now the question is: What ...
Soham Saha's user avatar
  • 1,434
0 votes
1 answer
29 views

Can a CL-term have multiple fixed points?

Given a CL term $E$, can there exist multiple non-equivalent fixed points for $E$? I think: any fixed point of $E$ can be expressed as $Y(E)$, this expression cannot reduce to multiple non-equivalent ...
Soham Saha's user avatar
  • 1,434
2 votes
1 answer
52 views

Checking equivalence of combinatorial terms.

Due to some context, I have reason to believe that S(K(SII)) and SSI are actually equivalent CL terms. This is my attempt at a proof (assuming a and b to be arbitrary CL terms): $$\text{S(K(SII))ab = ...
Soham Saha's user avatar
  • 1,434
1 vote
1 answer
60 views

Combinatory Logic Problem With Partial Reductions

I'm working through Bacon's Philosophical Introduction to Higher Order Logic. I am looking for help on the following problem: Exercise 3.17 Calculate the following, assuming that $\wedge : t \to t \...
C D's user avatar
  • 43
0 votes
0 answers
90 views

Combinators that form a 1-symbol basis of alternating associative combinatory logic

It is known that the combinators $S,K$ form a basis for lambda calculus. It's also known that the iota combinator $\lambda x.((x S) K)$ is a basis. Chris Barker found that the iota combinator allows a ...
Legendary Wizard's user avatar
1 vote
0 answers
42 views

Is there a combinator such that $M \rightarrow_w Μ$?

I am studying from Sorensen's book "Lectures on the Curry-Howard isomorphism" and it is there asked if there exists a combinator s.t. $M \rightarrow_w Μ$ (one step of weak reduction only), ...
Νικολέτα Σεβαστού's user avatar
2 votes
1 answer
81 views

SKI combinatory calculus, $M$ doesn't have a normal form. Find $(M S)$ that has a normal form

The problem is related to a similar question about lambda calculus. This question is about SKI combinatory calculus. I want to find a term $M$ without a normal form that will yield a term with a ...
Legendary Wizard's user avatar
2 votes
1 answer
116 views

Missing parentheses in $s(k (s I I))(s(\lambda y. s(k y))(\lambda y. s I I)$ leads to interesting error in an nLab page. Need a double check.

I think I found an error in the nLab page on partial combinatory algebra in the Example combinators section: Finally, consider the classical construction of the fixed-point combinator, $Y = \lambda y....
joseville's user avatar
  • 1,497
1 vote
1 answer
182 views

Beta reducing $SS(SK)$ using SKI calculus

I have an expression to $\beta$-reduce and I managed to brute force it using the $\lambda$-calculus. I was wondering though, if I could make it in less steps, than what I did, using the $SKI$-calculus....
Dknot's user avatar
  • 515
2 votes
1 answer
90 views

Doesn't lambda K-calculus include lambda I-calculus?

To mock a mockingbird, chapter 18: From just S and K you can derive any combinatorial bird whatsoever! Same book, chapter 19 […] with just the two birds J and I, we would ultimately get the same ...
Enlico's user avatar
  • 315
0 votes
1 answer
59 views

Nondeterminism In Modeling Computation with SKI-combinators

Consider two terms of the SKI-combinator calculus $\alpha$ and $\beta$ such that the following derivations are valid. $\alpha \rightarrow \alpha_1$ $\beta \rightarrow \beta_1$ Then we have two valid ...
Mark's user avatar
  • 5,812
3 votes
1 answer
336 views

SKI Calculus prefix notation of odd/even number

I'm working on a homework with SKI calculus. I saw the hints in this very useful post. We basically defined SKI functions as: ...
windweller's user avatar
2 votes
1 answer
92 views

Proof for $\frac{b}{h}=\frac{c(c-1)}{k(k-1)}$, a combinatorial identity

Imagine we have $b$ teachers and $c$ students in a school such that each teacher teaches $k$ students, every two students have $h$ similar teachers. I'd like to prove that $$\frac{b}{h}\:=\:\frac{c(...
Negar Rezaei Nejad's user avatar
9 votes
2 answers
254 views

What axioms can be added to $S,K$ combinator algebra without making it collapse into triviality?

My understanding is that if you start with the free magma on two generators (call them $S$ and $K$) and then take a quotient with respect to the usual $S$ and $K$ equivalence rules ($Sfgx = fx(gx)$ ...
J. Rees's user avatar
  • 91
2 votes
0 answers
83 views

An equation involving multisets

For multisets $A, B, C, A', B', C'$, if $A \uplus B \uplus \{B \uplus C\} \uplus \{A \uplus \{C\}\}$ = $A' \uplus B' \uplus \{B' \uplus C'\} \uplus \{A' \uplus \{C'\}\}$, must $A=A',B=B',C=C'$, where $...
Jeremy's user avatar
  • 529
4 votes
0 answers
211 views

Relationship between the semantics of simply typed lambda calculus and combinatory logic

The simply typed lambda calculus has a class of extremely intuitive models where each basic type $\sigma$ is modeled by some set $[\![\sigma]\!]$, and a complex type $\sigma\rightarrow\tau$ is then ...
R. Thomas's user avatar
  • 137
1 vote
0 answers
65 views

number of surjective functions from X to Y where card(Y)=k < n =card(X) [duplicate]

Let $X=\{1,...,n\}$ and $Y=\{1,...,k\}$. If $n\gt\ k$ then the number of surjective functions $f:X\to Y$ $\;\;$is $\;\sum_{j=0}^{k-1} (-1)^j\binom{k}{j}(k-j)^n$ Here I show what I have done. I can'...
user586431's user avatar
0 votes
0 answers
221 views

Hindley and Seldin "Introduction to Combinators and Lambda calculus": Question about the solution to exercise 3.5.

The question is concerning the solution to exercise 3.5. In the exercise, they ask us to prove that any finite set of simultaneous equations $x_iy_1...y_n=Z_i$, where $1\leq i\leq k$, can be solved ...
Tobias's user avatar
  • 13
0 votes
0 answers
42 views

Could we define an arity of a term in combinatory logic and consider some inference rule?

In computer science, we know a function has an arity. And we noticed the similarity between function and a term in combinatory logic, so could we define the arity of a term in combinatory logic? And ...
Mountain's user avatar
  • 540
2 votes
1 answer
104 views

How to define halting status in combinatory logic

We all know that combinatory logic can be used to express programs, for example: $S(K(SI))K\alpha\beta \rightarrow K(SI)\alpha(K\alpha)\beta \rightarrow SI(K\alpha)\beta ...
Mountain's user avatar
  • 540
3 votes
0 answers
659 views

Relation between Lambda calculus and SKI combinator calculus

I have played around with evaluation of Lambda terms in Lambda calculus and their counterparts using SKI combinators. While the results are extensionally equal (as they should be), there are striking ...
brunni's user avatar
  • 53
1 vote
1 answer
192 views

Would this be considered a combinator

A combinator is a function that doesn't utilize free variables. E.g. $$ \lambda a. \lambda b.a $$ However all of this works in an untyped environment. When working with types, let's say $nat$. can'...
hgiesel's user avatar
  • 1,257
0 votes
0 answers
143 views

Expressing I combinator and numerals via X combinator

So I understand that the X Combinator is defined as X = λx (x S) K I am also aware of definitions of S and K and I: S = XK <...
btrballin's user avatar
  • 249
27 votes
2 answers
2k views

Why can't we formalize the lambda calculus in first order logic?

I'm reading through Hindley and Seldin's book about the lambda calculus and combinatory logic. In the book, the authors express that, though combinatory logic can be expressed as an equational theory ...
Jacob Denson's user avatar
  • 2,139
1 vote
1 answer
299 views

The definition of the Church numerals in combinatory logic

Hindley & Seldin define ([1] Definition 4.2, p. 48) the Church numerals as follows: (I'm paraphrasing to save space. Here's the original page.) For every $n \in \{0,1,\dots\}$, the Church ...
Evan Aad's user avatar
  • 11.6k
1 vote
1 answer
465 views

How to prove the Church-Rosser theorem for combinatory logic

I need help proving the Church-Rosser theorem for combinatory logic. I will break down my post in three parts: part I will establish the notation required to state the Church-Rosser theorem as well as ...
Evan Aad's user avatar
  • 11.6k
2 votes
0 answers
43 views

Number of unique items in a big set from small sample

We have a box with $m=1\,000\,000$ cards. Each card contains one word. The words are repeated so there is a relatively small number of $n$ unique words. $n$ is unknown. If we get a sample of $k=5000$ ...
Pockets's user avatar
  • 21
1 vote
1 answer
622 views

Equality in the untyped lambda calculus without extensionality

Raymond Turner (in p.66 of "Truth and Modality for Knowledge Representation") elaborates a combinatory logic, $PT$, whose language $L2$ is the following language of terms (together with a language of ...
Luke's user avatar
  • 31
0 votes
1 answer
163 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: ...
metaphori's user avatar
  • 101
5 votes
0 answers
459 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). ...
dspyz's user avatar
  • 870
2 votes
1 answer
59 views

Rolling Dice Probability

A fair dice is rolled 3 times, The probability of the product of the three outcomes is a prime number is? The products which give a prime number I found out to be only 4. However for the total ...
user307178's user avatar
1 vote
0 answers
81 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 ...
Antonio Piccolomini d'Aragona's user avatar
2 votes
2 answers
433 views

An exercise on combinatory logic

Can somebody help me with the following exercise? (1) Find a combinator $X$ such that $Xy = X$; (2) Find a combinator in normal form with the same property. Rules for reduction are $Ix > x$ $Kxy &...
Antonio Piccolomini d'Aragona's user avatar
2 votes
1 answer
177 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(...
Antonio Piccolomini d'Aragona's user avatar
0 votes
0 answers
61 views

What is this P4 correspond to in proposition as types?

I was reading "Proofs and Types", so there came across that any proposition can be converted to lambda form. So was trying out with Hilbert system's axioms P1. $A \rightarrow A $ P2. $A \rightarrow (...
vinothkr's user avatar
  • 795
1 vote
1 answer
153 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?
Max's user avatar
  • 237
3 votes
1 answer
331 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 ...
PhD's user avatar
  • 2,771
7 votes
1 answer
1k views

Fixed point combinator (Y) and fixed point equation

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states: In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can ...
vinothkr's user avatar
  • 795
2 votes
1 answer
131 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$ and ...
vinothkr's user avatar
  • 795
8 votes
2 answers
2k 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 ...
dspyz's user avatar
  • 870
1 vote
1 answer
209 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 ...
user287393's user avatar
0 votes
1 answer
208 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 ...
Roy's user avatar
  • 747
7 votes
1 answer
440 views

Is there a proof of (non)existence of a proper universal combinator?

It is a well-known fact that all combinators can be derived from the two fundamental combinators K and S. It seems only natural to also ask whether there is a single universal combinator, but I can’t ...
user287393's user avatar
2 votes
1 answer
162 views

Chaitin's constant for lambda calculus and combinatory logic

I have found some approximations of Chaitin's Constant for turing machines but I have not found approximations for others. I'd like to have a rough estimate or upper bound on it for lambda calculus ...
Jake's user avatar
  • 461
5 votes
1 answer
490 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 ...
Josh Tilles's user avatar
6 votes
1 answer
763 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 ...
Johnny Bre's user avatar
1 vote
1 answer
174 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?
Trismegistos's user avatar
  • 2,420
22 votes
0 answers
557 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 ...
Steven Stadnicki's user avatar
5 votes
2 answers
248 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 ...
user avatar
3 votes
1 answer
167 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 ...
Wouter Stekelenburg's user avatar