Simplify K combinatory logic expression

Question

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-known S and K combinators have the following reduction rules:

$$ \begin{aligned} S\;x\;y\;z & \overset{S}{\implies} x\;z\;(y\;z) \\ K\;x\;y & \overset{K}{\implies} x \end{aligned} $$

A term is in normal form when no reduction is possible. A term has a normal form if a series of reductions applied to it gives a normal form. The halting problem in combinatory logic is essentially about determining whether a term has a normal form.

In a previous challenge of mine, I mentioned that the halting problem for K is trivial; it always terminates, and we can always find the normal form of a K expression.

Challenge

Given a K combinatory logic expression, simplify it into its normal form. For this challenge, the expression is to be input/output as a string (list of chars or charcodes is also acceptable), using prefix notation:

expr := "K" | "@" expr expr

So the expression \$K(KK)(KK)K\$ is given as @@@K@KK@KKK. The reduction rule can be also rewritten as

@@Kab => a

where a and b are valid expressions. The input is guaranteed to be a valid expression as a whole. You may use k instead of K, and any non-kK non-space printable ASCII character instead of @.

Standard code-golf rules apply. The shortest code in bytes wins.

Test cases

Generated using this Python script.

K -> K
@KK -> @KK
@K@KK -> @K@KK
@@KK@KK -> K
@@@@KK@KKKK -> K
@K@@@KKK@K@KK -> @K@K@K@KK
@@@KKK@@@KKK@@KKK -> @K@KK
@@@@@@@KK@KKK@@KK@@KK@KK@@@@KKK@@KKK@@K@KK@KKK@@@@K@@KK@KK@K@KK@@@KKK@K@K@KK@@@K@KK@K@K@KK@@@KK@@KK@KK@@KKK -> @K@K@K@K@KK

• Trebor: This is one of the great questions where an subject that is interesting on its own gets simplified to the point that it is not too simple and not too complicated for a code-golf.

Answer 1

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 normalizes to \$a_i = (\texttt{@K})^i\texttt K\$ for some \$i \ge 0\$, because \$\texttt K = a_0\$, \$\texttt @a_0a_j = a_{j + 1}\$, and \$\texttt @a_{i + 1}a_j \to a_i\$. So the innermost redex always looks like \$\texttt @(\texttt{@K})^{i + 1}\texttt K(\texttt{@K})^j\texttt K\$ for some \$i, j \ge 0\$, and reduces to \$(\texttt{@K})^i\texttt K\$.

To avoid the need to escape @K (which would otherwise refer to an array) as \@K, we relax it to .K, using backreferences for further copies. This doesn’t introduce bugs because any invalid redex \$\texttt @(\texttt{KK})^{i + 1}\texttt K(\texttt{KK})^j\texttt K\$ must be preceded by a valid redex \$\texttt @(\texttt{@K})^{i + 1}\texttt K(\texttt{@K})^j\texttt K\$.

• Arnauld: Is there any valid input that would fail with s/@(.K)(1円*K)1円*K/2ドル/? (I don't know why this @ has to be escaped in Perl to begin with, but ... so it is.)
• Anders Kaseorg: @Arnauld I think \@K → .K is fine there, by a somewhat complicated argument. Changed.
• hyperneutrino: You also don't need to use @; the challenge allows K/k for K and anything that isn't K/k for the apply token. If .K works, that's good too (I will admit I don't know why it works because I don't really understand this regex :P)

Answer 2

Haskell, 137 bytes

p('K':x)=(K,x)
p(_:x)|(s,z)<-p x,(u,v)<-p z=(s:@u,v)
data M=K|M:@M
f(x:@y)|K<-x="@K"++f y|K:@z<-x=f z|(u,_)<-p$f x=f$u:@y
f K="K"
f.fst.p

Try it online!

This one actually parses the strings into a tree. I'm sure this is not the most efficient way to do this but I actually couldn't beat it. p is our parser, and f performs the actual function.

Answer 3

Retina 0.8.2, 43 bytes

+`@@K(((@)|(?<-3>K))*(?(3)$)K){2}(?<-1>)
1ドル

Try it online! Link includes test cases. Explanation: The + simply repeats until the entire expression is normalised. The @@K represents a potential normalisation, but we still need to find a and b. The next portion of the regex achieves this by counting @s and Ks, stopping only after an equal number followed by a K. This is matched twice, but the second match b is then is dropped using (?<-1>), allowing the first match a to be used as the substitution.

Of course this is all blown out of the water when you consider @AndersKaesorg's observation that all you have to do is to normalise depth first for 20 bytes:

+`@(@K)(1円*K)1円*K
2ドル

Try it online! Link includes test cases.

• Neil: Note that you can replace the second and third K by \W which results in a program that can reduce arbitrary instances of Kab in expressions involving other terms, not just other K-expressions.

Answer 4

JavaScript (ES2019), 70 bytes

s=>(i=0,T=(p=s[i++],N=p<s?[p,p=T(),T()]:[p])=>p[1]>s?p[2]:N)().flat(i)

Try it online!

This one try to parse the string into a tree, and then convert back.

s=> // Input String
(i=0, // cursor for reading the string
T=( // We try to parse the string into a prefix expression tree
 // Tree structure would be `<exp> ::= ["K"] | ["@", <exp>, <exp>]`
p=s[i++], // get character under cursor, and move cursor to next character
N= // Node for expression tree
 p<s? // s would be a single "K" or start with "@"
 // In either cases, `p<s` indicate `p` is "@"
 [p, // Expression node, "@" character
 p=T(), // We reuse `p` variable to storage left child of current node
 T() // And right child here
 ]:
 [p] // `["K"]` as leaf node
)=>
 p[1] // If current character is "K", then p === "K", p[1] would be (void 0)
 // If current character is "@", then p is left child
 // If left child is leaf node ["K"], p[1] is (void 0)
 // If left child is non-leaf node ["@", <exp>, <exp>], p[1] is its left child
 >s? // p[1]>s whenever p[1] is "K" since s would start with "@"
 // For the special case s === "K", p[1] is (void 0) and compare would always be false
 p[2]: // Current node is ["@", ["@", "K", <exp = p[2]>], <exp>]
 // We keep p[2] and drop the right child expression
 N // Otherwise, we keep current expression as is
)().flat( // We flat the expression so we got an array of characters
 // which would be acceptable for string I/O
i) // `i` would equals to length of original string
 // And the expression nested level would always less than `i`
 // So we use `i` here to flatten the array

---

JavaScript (ES6), 51 bytes

f=s=>s<(s=s.replace(/@(@K)(1円*K)1円*K/,'2ドル'))?f(s):s

Try it online!

The regex used in this Perl answer.

Answer 5

Python 3, 82 bytes

import re
def f(e,n=1):
 while n:e,n=re.subn(r'@(@K)(1円*K)1円*K',r'2円',e)
 return e

Try it online!

Obligatory translation of Anders Kaseorg's excellent Perl solution. I will admit to not being sure this works.

Without regex:

Python 3, (削除) 125 (削除ここまで) (削除) 122 (削除ここまで) (削除) 97 (削除ここまで) (削除) 96 (削除ここまで) (削除) 94 (削除ここまで) 89 bytes

def f(e,*s):
 for x in e[::-1]:s=[x,*s]*(x>'@')or[s[0][2:]or'@K'+s[1]]+s[2:]
 return s[0]

Try it online!

-3 bytes because naming o was entirely pointless

-23 bytes thanks to tsh, and then I also shaved another 2 off since not needing list mutability opens the door to some splat abuse

-1 byte because it's not like s has to not be a list either

-2 bytes thanks to ovs replacing the ternary with another or

-5 porting Wheat Wizard's second golf to my Haskell solution

(Note: there are old explanations in the edit history)

def f(e ): # Define a function f taking an argument e
 ,*s # and collecting any extra arguments into a tuple s.
 # (There are no extra arguments, so s is empty.)
 for x in e[::-1]: # For each element x of e, in reverse order:
 s=[ ]*(x>'@') # if x is 'K', set s to a list
 x,*s # containing x followed by the elements of s,
 s= or # else set s to:
 [ ... ]+s[2:] # s without its first two elements, appended to:
 # (note: this would error if s was not a list,
 # but a valid input must end in K)
 s[0] # the first element of s
 [2:] # without its first two characters
 or # unless that's empty, otherwise
 '@K'+s[1] # the second element of s appended to 'K@'.
 return s[0] # Return the sole remaining element of s.

I'd attempted to remove the final reversal before, but it came out longer because I tried using insert instead of removing pop.

Since Python 2 doesn't require you to import reduce (why would they change that? :/ also thanks again to tsh), porting to it saves two more bytes:

Python 2, (削除) 93 (削除ここまで) (削除) 92 (削除ここまで) 86 bytes

lambda e:reduce(lambda s,x:([x]+s)*(x>'@')or[s[0][2:]or'@K'+s[1]]+s[2:],e[::-1],[])[0]

Try it online!

-1 porting ovs's golf

-5 porting Wheat Wizard's second golf to my Haskell solution

• tsh: 99 bytes
• Unrelated String: @tsh When I saw that you shaved 23 bytes off, I was worried I'd have to tell you to post it as your own answer, but that is a remarkably natural and obvious-in-retrospect golf to what I have. Thanks!
• tsh: 93 bytes in Python 2
• tsh: I don't quite understand what happened in these codes. I just try to strip some bytes from the original post. So I would not post it as another answer.
• ovs: 94 bytes by using or instead of if/else.

Answer 6

Haskell, (削除) 68 (削除ここまで) 64 bytes

head.foldr(#)[]
'K'#s="K":s
a#(t:n:s)|_:_:v<-t=v:s|u<-a:t++n=u:s

Try it online!

-4 thanks to Wheat Wizard actually using the destructured arguments and realizing that the input only consists of one expression (so at the end there should only be one on the stack)

Another translation of my Python answer.

 . -- The relevant function is the composition of
 foldr(#) -- right-associative folding #
 [] -- starting from an empty list
head -- and taking the first element from the result.
'K'#s= -- If the item encountered is the character 'K', # yields
 "K":s -- the string "K" prepended to the accumulator.
a# -- If it's something else (that is, '@', which we bind to a),
 (t:n: ) -- let t and n be the first two elements of the accumulator
 s -- and s the remaining elements;
 |_:_:v<-t -- if t has at least two elements to ignore let v be the rest
 =v:s -- and yield v prepended to s,
 |u<- -- else t must be "K", let u be
 a:t -- "@K"
 ++n -- concatenated with n
 =u:s -- and yield u prepended to s.

• Wheat Wizard: 2 bytes saved
• Wheat Wizard: And head is shorter than concat for another 2 bytes.

Answer 7

Python 3, 190 bytes

lambda x:h(c(g(x)))
g=lambda x:x.pop(0)>"@"and"K"or[g(x),g(x)]
c=lambda x:x=="K"and"K"or(lambda x:x[0][0]=="K"!=x[0]and x[0][1]or x)([*map(c,x)])
h=lambda x:x=="K"and x or"@"+h(x[0])+h(x[1])

Try it online!

Horribly long answer. But, it's the most direct way I could think of at first.

And a horribly scuffed one-liner using weird something-combinators just because this challenge is about combinators:

Python 3, 227 bytes

lambda x:(lambda h,c,g:h(h,c(c,g(g,x))))(lambda f,x:x=="K"and"K"or"@"+f(f,x[0])+f(f,x[1]),lambda f,x:x=="K"and"K"or(lambda x:x[0][0]=="K"!=x[0]and x[0][1]or x)([f(f,y)for y in x]),lambda f,x:x.pop(0)>"@"and"K"or[f(f,x),f(f,x)])

Try it online!

Answer 8

Jelly, (削除) 22 (削除ここまで) 21 bytes

Ṫṫ3ȯṪ)0K;Ɗṭ
ṚṭÇ}V?@/Ṛ

Try it online!

A full program that takes a single argument consisting of Ks and 0s and prints the output to STDOUT using the same symbols.

Based on @UnrelatedString’s Python answer so be sure to upvote that one too!

Thanks also to @UnrelatedString for saving a byte!

Explanation

Helper link

Takes the current draft output list and processes it where there was a zero in the next position

Ṫ | Tail (pop last element from list)
 ṫ3 | Third character onwards
 ȯ Ɗ | Or the following as a monad:
 Ṫ | - Tail (pop last element from list)
 )0K; | - Concatenate "0K" to this
 ṭ | Tag onto end of draft output list (this will have lost its last two members via the action of Ṫ twice)

Main link

Ṛ | Reverse
 @/ | Reduce using the following, swapping left and right arguments:
 V? | - If the next value in the reversed list evaluates to non-zero (i.e. is a K)
 ṭ | - Then wrap it in a list and add to the end of the draft output list
 Ç | - Otherwise call helper link on draft output list
 Ṛ | Finally reverse, and implicitly smash together and print

• Unrelated String: -1. Nice job thinking to use / over ƒ, by the way--it took me a while to realize why that worked, even though I already had to count on the last element being K for my Python solution
• Unrelated String: -1 byte, +1 vote ;)
• Nick Kennedy: @UnrelatedString thanks! Completely missed the link there...

Answer 9

Jelly, 20 bytes

OḂU;Ṫ’o+ɗṪṭƲṛ?/ṬCṫ@Q

Try it online!

Stumbled back on this challenge yesterday (due to having a few too many tabs open), and decided I'd try a solution that treats the output as numeric before reconstituting to an expression at the end. After quite a few sporadic insights--many of which turned out to be wishful thinking, but the most crucial of which was simply not inverting the bits of the processed input--it just barely beats Nick Kennedy's excellent existing Jelly solution.

OḂ Parity bit of each codepoint: @ -> 0, K -> 1
 U Reverse
 / and reduce left to right:
 ṛ? if the right argument / current new element is 1,
 ; append it to the stack,
 ṭ else append
 Ṫ the popped top of the stack
 ’ decremented
 o unless that's 0, in which case use
 +ɗ its sum with
 Ṫ Ʋ the popped new top of the stack.
 Ṭ Untruth the single remaining element (n-1 0s and a 1),
 C subtract from 1,
 ṫ@ and for each give that many elements from the end of
 Q the uniquified input ("@K" unless we don't need it).

This essentially treats @K as an "increment" instruction, K as the number 1, and @ on anything other than K/1 as "decrement top and pop second from top".

Answer 10

Curry (PAKCS), 60 bytes

f"K"="K"
f('@':a++b)=(f a!)$!f b
"K"!b="@K"++b
("@K"++a)!_=a

Attempt This Online!