Skip to main content
The 2024 Developer Survey results are live! See the results

Questions tagged [combinatory-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
0 answers
42 views

What rules govern when combinators (e.g. S, K, and I) can be only partially applied?

In the Wikipedia page on the SKI combinator calculus, an example is given of two equivalent reductions of the expression SKI(KIS) [0]. In both cases, ...
jpt4's user avatar
  • 109
2 votes
0 answers
149 views

How to implement the next type inference algorithm?

Here I mean only simple typed Lambda calculus / Combinatory logic. Notation: Combinatory logic terms: $F, X_i, Y_i$. Term application: $(F*X_1)$. Type variables $x_i,y_i$. Type assignment: $X:x_i$. ...
Oleg Dats's user avatar
  • 121
9 votes
0 answers
208 views

Is it known how much computation a fixed-point combinator gets you?

It is well-known that the SKI combinators are enough to get universal computation, though the original version of combinatory calculus used BCKW. However, it is possible to get a fixed-point ...
David Roberts's user avatar
2 votes
0 answers
478 views

Is Combinatory Logic (CL) still relevant for programming language theory?

I've been reading up on R. Smullyan's "To Mock a Mockingbird" and Hindley's "Lambda-Calculus and Combinators: An Introduction". I've even read Schonfinkel's 1924 paper introducing the idea of ...
PhD's user avatar
  • 5,335
14 votes
1 answer
4k views

What is the "question" that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
PhD's user avatar
  • 5,335
1 vote
0 answers
190 views

translation of first-order logic to combinatory logic

I am new to combinatory logic, and I am interested in its relationship to first-order logic. In particular, I am wondering if there is a universal translation of first-order logic to combinatory logic ...
bluether's user avatar
4 votes
0 answers
87 views

Can any Calculus of Construction term be built up from application of a finite number of terms?

Can we form a finite set of well typed calculus of construction terms such that any closed term can be built up from them (plus the type of large types) using only application? I conjecture that the ...
Christopher King's user avatar
17 votes
1 answer
1k views

How can non-terminating $\lambda$-terms be turned into fixed-point combinators?

I've been thinking about these questions: Is there a typed lambda calculus which is consistent and Turing complete? https://cs.stackexchange.com/questions/65003/if-%CE%BB-x-x-x-has-a-type-then-is-...
cody's user avatar
  • 14k
5 votes
0 answers
107 views

Characterisation of the BCIW definable functions

Given a full model of the simply typed lambda calculus, it's possible to characterise the lambda definable functions as those that are invariant under every "Kripke logical relation". (See here.) I ...
Andrew Bacon's user avatar
12 votes
1 answer
517 views

Incomplete basis of combinators

This is inspired by this question. Let $\mathcal{C}$ be the collection of all combinators which only have two bound variables. Is $\mathcal{C}$ combinatorially complete? I believe the answer is ...
user avatar
2 votes
2 answers
288 views

Algorithm for extensional equality in combinator calculus

I'm dealing with combinator calculus, using the $S$ and $K$ combinators as a basis. Sometimes my code generates expressions that define equivalent functions, such as $$ (S\, K\, K) \qquad\text{and}\...
N. Virgo's user avatar
  • 719
7 votes
2 answers
792 views

Concatenative binary lambda calculus/combinatory logic

John Tromp defines a version of the lambda calculus that is encoded in binary: https://tromp.github.io/cl/cl.html a) Does there exist a concatenative version of this language (or its combinatory ...
NietzscheanAI's user avatar
21 votes
3 answers
2k views

Smallest possible universal combinator

I am looking for the smallest possible universal combinator, measured by the number of abstractions and applications required to specify such a combinator in the lambda calculus. Examples of universal ...
user76284's user avatar
  • 672
8 votes
3 answers
1k views

What is the relationship between intuitionistic logic, combinatory logic and lambda calculus?

I've been reading Lectures on the Curry-Howard Isomorphism and it talks about intuitionistic/constructive logic (IL) , combinatory logic (CL) and lambda calculus ($\lambda$c) before moving on to the ...
PhD's user avatar
  • 5,335
8 votes
1 answer
341 views

Church-Rosser equivalent for concatenative languages?

Looking at the striking parallels between combinatory logic and concatenative languages makes me wonder how many theorems of the former hold in the latter. The Church-Rosser theorem is particularly ...
user287393's user avatar
7 votes
1 answer
188 views

Upper bound on Chaitin's constant for lambda calculus and SKI combinatory logic

I'd like to have proof that Chaitin's constant for lambda calculus and/or SKI combinatory logic is pretty small. I've found some approximations (accurate to about 63 binary digits) for truing machines ...
Jake's user avatar
  • 1,213
8 votes
0 answers
528 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
Jake's user avatar
  • 1,213
5 votes
1 answer
198 views

Is combinatory strong reduction equivalent to lambda beta-eta reduction?

I'm familiar with the correspondence between combinatory logic and $\lambda$-calculus at equality level, ie $=_{\beta\eta}$ corresponds to $=_s$ (the equivalence relation generated by strong reduction)...
Martha S.'s user avatar
-1 votes
1 answer
55 views

Algorithm for calculating substitution combination with ordering

I need to calculate the combinations of elements with a substitution element. For example for elements [A,B] if the substitution is X the results should be ...
Thihara's user avatar
  • 101
2 votes
2 answers
743 views

Size of decision tree for f is polynomial in the DNF size of f and CNF size of f

I've been having hard time with proving the following claim: Let $f:\{T,F\}^n\rightarrow \{T,F\}$ be a boolean function. Let $size_{DT}(f)$ denote the number of leaves in the smallest (w.r.t the ...
user13772's user avatar
8 votes
1 answer
402 views

Is there a normalizing (or perpetual) reduction strategy for untyped combinators?

Inspired by this question, I was curious whether there was a reduction strategy for untyped SKI combinators that was known to be either normalizing or perpetual. As described here (Twelfed here), ...
Rob Simmons's user avatar
  • 2,396
30 votes
2 answers
4k views

Are lambda calculus and combinatory logic the same?

I am currently reading "Lambda-Calculus and Combinators" by Hindley and Seldin. I'm not an expert, but have always taken an interest in lambda calculus because of involvement with functional ...
Shane's user avatar
  • 2,233
22 votes
2 answers
2k views

Succinct circuit representation of graphs

The complexity class PPAD (e.g. computing various Nash equilibria) can be defined as the set of total search problems polytime reducible to END OF THE LINE: END OF THE LINE: Given circuits S and P ...
Daniel Apon's user avatar
  • 6,011