Questions tagged [combinatory-logic]
For challenges pertaining to Combinatory Logic model of computing.
16
questions
18
votes
1
answer
776
views
Largest SKI output in less than 200 combinators
The Challenge
Create an terminating expression in SKI Combinator Calculus in less than 200 combinators (S, K, I) that reduces to the expression with the most combinators.
There will be no limit on how ...
- 743
5
votes
1
answer
284
views
Tips for Golfing the Lambda Calculus & Friends
This includes tips for all related derivatives, as coding in these langs often primarily consists of writing the function in the lambda calculus and then compiling it down at the end.
Among others, ...
- 2,111
12
votes
2
answers
1k
views
SKI calculus golf: Hello, World!
Background
SKI combinator calculus, or simply SKI calculus, is a system similar to lambda calculus, except that SKI calculus uses a small set of combinators, namely ...
- 73.8k
6
votes
4
answers
251
views
Ordered, linear, affine, or relevant?
Background
Supplementary reading 1, Supplementary reading 2
Linear lambda calculus is a limited form of lambda calculus, where every bound variable must be used exactly once. For example, ...
- 73.8k
17
votes
2
answers
851
views
We all know how to SKI, but can you BCKW?
Background
Lambda calculus is a model of computation using lambda terms.
A variable \$x\$ is a lambda term.
If \$E\$ is a lambda term, the lambda abstraction \$\lambda x. E\$ is a lambda term.
If \$...
- 73.8k
14
votes
8
answers
832
views
Simplify K combinatory logic expression
Background
Combinatory logic is a system where a term is written using a finite set of combinators and function application between terms, and reduction rules are defined for each combinator. The well-...
- 73.8k
16
votes
2
answers
361
views
Solve the halting problem for S combinatory logic
Background
Combinatory logic is a system where a term is written using a finite set of combinators and function application between terms, and reduction rules are defined for each combinator. The well-...
- 73.8k
14
votes
2
answers
472
views
Insert parens into a free-form SKI calculus expression
Imagine a simple SKI calculus expression - for example, (((S α) β) γ). As you can see, each node of the rooted tree has exactly two children. Sometimes though, the ...
- 12.2k
15
votes
13
answers
2k
views
Implement SKI combinator calculus
This challenge is to golf an implementation of SKI formal combinator calculus.
Definition
Terms
S, K, and ...
- 1,438
20
votes
4
answers
1k
views
SKI calculus golf: Half of a Church numeral
Background
SKI combinator calculus, or simply SKI calculus, is a system similar to lambda calculus, except that SKI calculus uses a small set of combinators, namely ...
- 73.8k
42
votes
3
answers
2k
views
(A → B) → (¬B → ¬A)
Well I think it is about time we have another proof-golf question.
This time we are going to prove the well known logical truth
\$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)\$
To do ...
- 96.5k
22
votes
1
answer
2k
views
Convert λ-expressions to SK-expressions
The λ-calculus, or lambda calculus, is a logical system based on anonymous functions. For example, this a λ-expression:
λf.(λx.xx)(λx.f(xx))
However, for the ...
- 15.4k
13
votes
3
answers
844
views
Combinatory Conundrum!
Introduction: Combinatory Logic
Combinatory logic (CL) is based off of things called combinators, which are basically functions. There are two basic "built-in" combinators, ...
- 6,972
24
votes
4
answers
1k
views
Optimizing SKI compiler
The SKI calculus is a variant of the Lambda calculus that doesn't use lambda expressions. Instead, only application and the combinators S, K, and I are used. In this challenge, your task is to ...
- 10.1k
13
votes
2
answers
661
views
Combinator quines
Background
You have just learned what combinatory logic is. Intrigued by the various combinators you spend quite a bit of time learning about them. You finally stumble upon this particular expression:...
- 1,485
9
votes
5
answers
370
views
Write biSp in point-free form using as few terms as possible
The Haskell function biSp has type signature
...
- 935