Curry (PAKCS), 60 bytes

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

Attempt This Online!

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".

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

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.

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

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

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.

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.

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.

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!