# Tag Info

### (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 ...
• 39.7k

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

91 Steps Full Proof: ...

### Largest SKI output in less than 200 combinators

44 combinators, score: $\approx f_{\omega+1}(3\uparrow\uparrow\uparrow\uparrow3)$ ...
• 77.1k

### (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....

### 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 ...
• 39.7k

Score = 192 ...
• 39.7k

### Implement SKI combinator calculus

Seed, 5925 5909 5890 5871 bytes ...
• 12.4k

### 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 ...
• 12.4k
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 ...
• 4,115

• 39.7k
Accepted

### Evaluate Ternary Logic

Vyxal 3, 1 byte Ė Try it Online! Accepts input in reverse polish notation with LT represented by ...
• 42.4k

• 172k

### 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 ...
• 141
Accepted

• 39.7k