The 2024 Developer Survey results are live! See the results

Questions tagged [combinatory-logic]

The tag has no usage guidance.

23 questions
Filter by
Sorted by
Tagged with
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, ...
• 109
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$. ...
• 121
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 ...
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 ...
• 5,335
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 ...
• 5,335
1 vote
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 ...
• 11
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 ...
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-...
• 14k
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 ...
• 453
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 ...
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}\...
• 719
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 ...
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 ...
• 672
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 ...
• 5,335
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 ...
• 181
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 ...
• 1,213
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 ...
• 1,213
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)...
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 ...
• 101
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 ...
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), ...
• 2,396
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 ...
• 2,233