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

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\$.

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.

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

Answer 6

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 7

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

Answer 8

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.