Questions tagged [combinatory-logic]
Combinatory logic, combinatorial calculi, and other questions about combinators and variable-free variants of the $\lambda$-calculus.
40
questions
9
votes
2answers
190 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)$ ...
2
votes
0answers
69 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 $...
4
votes
0answers
77 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 ...
1
vote
0answers
51 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'...
0
votes
0answers
121 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 ...
0
votes
0answers
28 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 ...
1
vote
1answer
69 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
...
2
votes
0answers
247 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 ...
1
vote
1answer
93 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'...
0
votes
0answers
82 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 <...
16
votes
0answers
929 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 ...
1
vote
1answer
201 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 ...
1
vote
1answer
295 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 ...
2
votes
0answers
39 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$ ...
1
vote
1answer
295 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 ...
0
votes
1answer
93 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: ...
4
votes
0answers
340 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).
...
2
votes
1answer
43 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 ...
1
vote
0answers
63 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 ...
2
votes
2answers
342 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 &...
2
votes
1answer
136 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(...
0
votes
0answers
50 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 (...
1
vote
1answer
52 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?
3
votes
1answer
238 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 ...
6
votes
1answer
692 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 ...
2
votes
1answer
78 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 ...
5
votes
2answers
1k 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 ...
1
vote
1answer
150 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 ...
0
votes
1answer
194 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 ...
5
votes
1answer
285 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 ...
2
votes
1answer
117 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 ...
4
votes
1answer
435 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 ...
5
votes
1answer
691 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 ...
1
vote
1answer
124 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?
17
votes
0answers
463 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 ...
5
votes
2answers
205 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 ...
4
votes
1answer
137 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 ...
3
votes
1answer
4k 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 ...
30
votes
3answers
6k 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 ...
1
vote
2answers
1k 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).
