# Questions tagged [combinatory-logic]

The tag has no usage guidance.

20 questions
Filter by
Sorted by
Tagged with
189 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 ...
1k 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 ...
135 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 ...
75 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 ...
704 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-...
84 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 ...
287 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 ...
164 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}\...
322 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 ...
1k 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 ...
961 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 ...
278 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 ...
151 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 ...
406 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 ...
164 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)...
49 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 ...
529 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 ...
284 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), ...