Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [combinatory-logic]

For questions about logical systems defined via the application and term-rewriting of combinators. These systems often have a close connection to the lambda calculus.

0
votes
0answers
43 views

Does a Turing complete set of invertible combinators exist?

We'll say that a combinator A is invertible if there exists A' s.t. A'(Ax) = A(A'x) = x For example, Sxyz = xz(yz) is clearly invertible in this sense because we ...
5
votes
1answer
48 views

Find a lambda term satisfying two equations

I'm just looking for the general idea on how to approach the following problem: Find a term $\Delta=\lambda x.xUV$ such that: $\Delta\Delta=K$ $\Delta K=S$ (it's a system of 2 equations, I didn't ...
1
vote
0answers
19 views

Combinatory Logic formula obtained from lambda term, proof?

I translated the following $\lambda$-term: $z(\lambda b.ba)(tt)(\lambda y.y)$ in the following CL formula: $z(CIa)(tt)I$ through the Markov algorithm. Now I'd like to prove the translation was ...
1
vote
0answers
26 views

Job shop scheduling with events that should be completed simultaneously

I'm working on a scheduling algorithm that schedules a set of events with an event duration to a set of agents with various working times. However, some events require more than one agent to be ...
1
vote
0answers
65 views

Combinatory logic equivalent to System F

Simply typed lambda calculus has a combinatory logic equivalent with the same expressive power without the need of defining names via lambda abstraction. Is there a formalism as powerful as System F ...
1
vote
1answer
51 views

Is there a combinator that introduces brackets to a combinatory logic expression using just B?

Suppose I have the expression $abcdef$ and I want a combinator $X$ that does this: $Xabcdef=a(bcd)(ef)$. Is it possible to express $X$ using just the $B$ combinator, defined by $Babc=a(bc)$? Is ...
1
vote
0answers
73 views

Is $(X (X X)) ((X X) X) X$ the most simple representation of the identity combinator when $X = \lambda x . x KSK$?

Let combinator $X = \lambda x . x KSK$ as described by Hankin (1994). Then $K = (X X) X$ and $S = X(X X)$. Identity combinator however seems to have much more verbose form. If $I = SKK$ then also $$...
1
vote
1answer
62 views

Trouble Replicating Proof of The Lambda Calculus Fixed Point Theorem

From pg. 35 of Lambda Calculus and Combinators An Introduction: Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0$, the equation $$ xy_1 \ldots y_n = Z $$ can be solved ...
1
vote
0answers
22 views

How to interpret scoped variables next to each other within Lambda Terms and CL-terms?

In both the lambda calculus ($\lambda$-calculus) and Combinatory Logic (CL), we have the notion of function application. For example: \begin{array} & \left( \lambda x . x \right) y = y & \...
3
votes
1answer
71 views

Understanding A Recursive Definition of CL-Terms in Combinatory Logic

From page 26 of Lambda-Calculus and Combinators: Definition 2.18 (Abstraction) For every CL-term $M$ and every variable $x$, a CL-term called $[x].M$ is defined by induction on $M$, thus: (a)...
9
votes
1answer
299 views

Simplest complete combinator basis pair for flat expressions

In Chris Okasaki's paper "Flattening Combinators: Surviving Without Parentheses" he shows that two combinators are both sufficient and necessary as a basis to encode Turing-complete expressions ...
2
votes
0answers
29 views

The range of functions defined by pure lambda terms

Consider a full set-theoretic model of the simply typed $\lambda$-calculus with infinite base types. Say that an element in this model is pure if it is the semantic value of some closed pure term in ...
10
votes
0answers
122 views

When can you “invert” an equation in the lambda calculus

Suppose that $M$ is a full model of the simply typed lambda calculus. Suppose each base type is infinite. Now suppose that $f$ and $g$ are two functions in $M$ (not necessarily in the same domain) ...
17
votes
2answers
524 views

Basis sets for combinator calculus

It is well known that the S and K combinators form a basis set for combinator calculus, in the sense that all other combinators can be expressed in terms of them. There is also Curry's B, C, K, W ...
13
votes
1answer
211 views

What functions can combinator calculus expressions compute?

A combinator expression (let's say in the SK basis) can be thought of as a function that maps combinator calculus expressions to combinator calculus expressions. That is, one can think of an ...
6
votes
1answer
193 views

Combinator equivalent to eta conversion

In lambda calculus, one can prove that two expressions compute the same function if they are equivalent under both beta reduction and eta conversion, where eta conversion consists of eta reduction, $$ ...
8
votes
3answers
2k views

What is the purpose of the SKI combinator calculus(or even lambda calculus)? What are some real life examples of its use?

I understand what it is, but I don't see how it is any use for algorithms or anything. Maybe I am missing something. I need someone to give me an example of how it can be used so I can understand it ...
2
votes
0answers
40 views

Computing the index in a structured way

I want to map the various combinations to an unique index: For a given $n$ and $r$, we would have $\binom{n}{r}$ arrangement for values:$[0,\dots,n)$: Ex: For n = 6, r = 3 [012, 013, 014, 015, ..., ...
3
votes
1answer
337 views

Iota combinator and implicational propositional calculus

There is are two esoteric languages with minimally functionally complete operators, iota and jot, that are closely related to SK combinators. I'm attempting to understand the relationship between ...
1
vote
1answer
35 views

“Archiving” byte sequence into human-readable set of chars

Ok, lets assume we have sequence of 1000 bytes. So the possible number of value variations is 2^100. Is there a way to "index" each variation with letters and decimal numbers (A-Z, 0-9), having as ...
9
votes
1answer
262 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...
2
votes
1answer
139 views

Smallest non-halting unlambda program

Is ```sii``sii the smallest Unlambda program that doesn't halt? In other words, what is the smallest non-terminating combinator term in SKI augmented with $C$ (...
10
votes
2answers
274 views

Combinatory interpretation of lambda calculus

According to Peter Selinger, The Lambda Calculus is Algebraic (PDF). Early in this article he says: The combinatory interpretation of the lambda calculus is known to be imperfect, because it does ...