Skip to main content
28 votes

(A → B) → (¬B → ¬A)

88 82 77 72 steps Thanks to H.PWiz for better combinator conversions that saved 10 steps! Explanation You might be familiar with the Curry–Howard correspondence, in which theorems correspond to ...
Anders Kaseorg's user avatar
26 votes

(A → B) → (¬B → ¬A)

91 Steps Full Proof: ...
Tipping Octopus's user avatar
21 votes

Largest SKI output in less than 200 combinators

44 combinators, score: \$\approx f_{\omega+1}(3\uparrow\uparrow\uparrow\uparrow3)\$ ...
Bubbler's user avatar
  • 77.1k
19 votes

(A → B) → (¬B → ¬A)

59 steps Norman Megill, author of Metamath has told me about a 59 step proof, which I'm going to post here in this community wiki. The original can be found in theorem 2.16 on this page. http://us....
15 votes

SKI calculus golf: Half of a Church numeral

40 combinators S(S(SI(K(S(S(KS)K)(K(S(S(KS)(S(KK)S))(K(S(KK)(S(S(KS)K)))))))))(K(S(SI(K(KI)))(K(KI)))))(KK) Try it online! Generated with a little help from a ...
Anders Kaseorg's user avatar
15 votes

SKI calculus golf: Hello, World!

Score = 192 ...
Anders Kaseorg's user avatar
14 votes

Implement SKI combinator calculus

Seed, 5925 5909 5890 5871 bytes ...
Kamila Szewczyk's user avatar
11 votes

Implement SKI combinator calculus

C (gcc), 666 616 518 483 476 bytes Who doesn't love classy, Arthur Whitney-styled code? No regular expressions involved, only clever parsing and evaluation. PS: Yes, obviously, a few bytes can be ...
Kamila Szewczyk's user avatar
10 votes
Accepted

Implement SKI combinator calculus

Wolfram Language, 63 bytes #//.{{I,x_}->x,{{K,x_},y_}->x,{{{S,x_},y_},z_}->{{x,z},{y,z}}}& Try it online! God, I love pattern matching in Wolfram ...
DanTheMan's user avatar
  • 4,115
9 votes

Simplify K combinatory logic expression

Perl 5 -p, 28 27 bytes s/@(.K)(\1*K)\1*K/$2/&&redo Try it online! How it works Each term in the \$K\$ calculus ...
Anders Kaseorg's user avatar
9 votes

Solve the halting problem for S combinatory logic

Charcoal, 264 260 257 235 bytes ...
Neil's user avatar
  • 172k
9 votes

Convert λ-expressions to SK-expressions

Haskell, 251 237 222 214 bytes 15 bytes saved thanks to @Ørjan_Johansen (also see his TIO links in the remarks)! 8 more bytes saved thanks to @nimi! ...
Christian Sievers's user avatar
8 votes

Combinatory Conundrum!

Haskell, score 5017 This combines the dumbest possible algorithm for abstraction elimination ((λx. x) = I; (λx. y) = Ky; (λx. M N) = S(λx. M)(λx. N)) with a peephole optimizer used after every ...
Anders Kaseorg's user avatar
8 votes

Combinator quines

Cycle: \$f_{\omega^{\omega^{\omega^{\omega^\omega}}}}(65536)\$, combinators: 98 ...
2014MELO03's user avatar
  • 1,051
7 votes

We all know how to SKI, but can you BCKW?

Haskell, 133 bytes data T=T:@T|L T|V Int|B|C|K|W l(x:@y)=W:@(B:@(C:@l x):@l y) l(V 0)=W:@K l(V n)=K:@V(n-1) l x=K:@x f(L x)=l$f x f(x:@y)=f x:@f y f x=x Try it ...
Anders Kaseorg's user avatar
7 votes
Accepted

Evaluate Ternary Logic

Vyxal 3, 1 byte Ė Try it Online! Accepts input in reverse polish notation with LT represented by ...
hyper-neutrino's user avatar
  • 42.4k
5 votes

Insert parens into a free-form SKI calculus expression

Perl 5 -p, 37 bytes s/(\w|\((?1)*\)){2}(?!\))/($&)/&&redo Try it online!
Anders Kaseorg's user avatar
5 votes

Implement SKI combinator calculus

Rust Macros, 480 441 bytes ...
Aiden4's user avatar
  • 2,465
5 votes

Combinatory Conundrum!

Sum of solution lengths: 12945 8508 5872 Haskell code that takes input lines from stdin and doesn't care if the separator is = or ...
Christian Sievers's user avatar
4 votes

SKI calculus golf: Half of a Church numeral

31 combinators S(S(S(SI(K(S(S(KS)(S(KK)S))(K(S(KK)(S(S(KS)K)))))))(KK))(K(KI)))(K(KI)) Try it online! $$\begin{align*} \textit{zero} &= λf. λx. x = KI \\ \...
2014MELO03's user avatar
  • 1,051
4 votes

Implement SKI combinator calculus

APL (Dyalog Unicode), 127 124 bytes Full program. No use of regex. ...
Adám's user avatar
  • 30.4k
4 votes

Simplify K combinatory logic expression

Haskell, 137 bytes ...
Wheat Wizard's user avatar
  • 98.8k
4 votes

We all know how to SKI, but can you BCKW?

Python 3, 451 bytes ...
Adalynn's user avatar
  • 6,132
4 votes

SKI calculus golf: Hello, World!

5844 SKIs The Baseline In order to respect your scrolling fingers, I won't copy & paste it here. The 5,844 score is the SKI count; it doesn't even include all the parentheses. But please do try it ...
AviFS's user avatar
  • 2,111
4 votes

Evaluate Ternary Logic

Python 2, 52 bytes f=lambda s:s.pop(0)(f(s),f(s))if 1<s[0]else s.pop(0) Attempt This Online! Takes input in Polish notation with the following mapping: ...
Mukundan314's user avatar
  • 12.3k
4 votes

Evaluate Ternary Logic

Retina 0.8.2, 88 bytes {`(?=(S.?L|S.?E?|B.?G|B.?E?|OE?.|CE.|CLG|CGL)(?<=(.))).[GEL]{2} $2 CGE L CLE G CLL|CGG E Try it online! Link includes test cases. Key: <...
Neil's user avatar
  • 172k
3 votes

Implement SKI combinator calculus

Wolfram Language, 44 bytes s[a_][b_][c_]:=b@c//a@c;k[a_][b_]:=a;i@a_:=a This defines them as actual functions in Wolfram, so ...
Trev's user avatar
  • 141
3 votes
Accepted

Optimizing SKI compiler

Haskell, 232 bytes ...
Anders Kaseorg's user avatar
3 votes

Combinatory Conundrum!

8486 using S, K, I, W Explanation The standard algorithm (as described e.g. in chapter 18 of To Mock a Mockingbird) uses four cases, corresponding to the combinators ...
Peter Taylor's user avatar
  • 43.1k
3 votes

Implement SKI combinator calculus

Retina 0.8.2, 171 bytes ...
Neil's user avatar
  • 172k

Only top scored, non community-wiki answers of a minimum length are eligible