<p>Not good with proofs but can answer number 2.</p>
<p>First of all it isn't necessary to use a complicated compilation scheme, you can just use PHOAS or a tagless final style directly.</p>
<pre><code>class Category k =&gt; Terminal k where
     bang :: k a ()
class Terminal k =&gt; Kappa k where
     kappa :: (k () a -&gt; k b c) -&gt; k (a, b) c
     lift :: k () a -&gt; k b (a, b)
</code></pre>
<p>I literally find this nowhere but there's a dual zeta calculus that composed with the Kappa calculus gives you a full lambda calculus</p>
<p><a href="http://www.kurims.kyoto-u.ac.jp/%7Ehassei/papers/ctcs95.html" rel="nofollow noreferrer">http://www.kurims.kyoto-u.ac.jp/~hassei/papers/ctcs95.html</a></p>
<pre><code>class Terminal k =&gt; Zeta k where
    zeta :: (k () a -&gt; k b c) -&gt; k b (a -&gt; c)
    pass :: k () a -&gt; k (a -&gt; b) b

class (Kappa k, Zeta k) =&gt; Lambda k
</code></pre>
<p>The dual constructions are literally just the same things but in the opposite category</p>
<pre><code>class Category k =&gt; Initial k where
    absurd :: k Void a
class Initial k =&gt; Sum k where
     label :: (k a Void -&gt; k c b) -&gt; k c (a + b)
     jump :: k a Void -&gt; k (a + b) b
class Initial k =&gt; Coexponential k where
     cozeta :: (k a Void -&gt; k b c) -&gt; k (b -&lt; c) a
     compass :: k a Void -&gt; k b (a -&lt; b)
class (Sum K, Coexponential k) =&gt; Colambda k
</code></pre>
<ul>
<li>would be a type synonym for Either probably. -&lt; would have to be a phantom type</li>
</ul>
<p>You would want to add Sum into the mix but not Coexponential which is basically just as powerful as exponentials but just really really strange.</p>
<p>Incidentally, you can't exactly really usefully have both exponentials and coexponentials in a programming language unless you have some sort of linear type system or something, not sure of the precise details.</p>
<p>Sum + Kappa is still not Turing complete IIRC.</p>
<p>If you had a Fixpoint type that is equivalent in power to a Fixpoint operater IIRC.</p>
<p>But I'm not sure that works without exponentials.</p>

CC BY-SA 4.0
2020-12-16T04:53:26.250Z
2020-12-16T04:53:26.250Z
Ms. Molly Stewart-Gallus
<p>The bare $\kappa$-calculus does not permit defining factorial, even when extended with a fixed point operator. However, this answer deserves some unpacking. </p>

<ol>
<li><p>The fixed point operator you give is not well-formed according to the grammar of types in the $\kappa$-calculus. Note that the grammar of types does not contain the function space $\tau \Rightarrow \tau'$ -- this is because the $\kappa$-calculus is a language of <em>first-order</em> functions. An expression has a type $\tau_1 \to \tau_2$, to indicate that it is an expression of type $\tau_2$, whose free variables are typed by $\tau_1$. </p>

<p>The proper typing for a fixed point operator would be roughly something like:
$$
\frac{\Gamma, x:1 \to \tau \vdash e : 1 \to \tau}
     {\Gamma \vdash \mu x:1 \to \tau. e : 1 \to \tau}
$$</p></li>
<li><p>Once you've fixed this, you still can't define a factorial.</p>

<p>The plain $\kappa$-calculus does not have sums or natural numbers as a base type. As a result, you can't write branching programs, and so you cannot define interesting recursive functions. If you added natural numbers and their iterator, you could define a factorial function. Hasegawa actually gives factorial as an example in his paper on the $\kappa$-calculus, in a calculus augmented with a basic natural number type.</p>

<p>However, you might wonder why you <em>are</em> able to define factorial in the pure lambda calculus, even though it has no apparent control structures. The reason is that the interaction of fixed points and recursion gives you a "universal type" (i.e., a type $V$ such that $V$ is isomorphic to $V \to V$), and this lets you encode any datatype as a subset (more accurately, a retract) of it. </p>

<p>In more syntactic terms, you can write the Y combinator (i.e., Curry's paradox) in any language with (a) higher-order functions, (b) recursion, and (c) the ability to use each variable more than once in a program. Since the basic $\kappa$-calculus lacks (a), adding even an unrestricted fixed point operator does not make it Turing-complete! </p></li>
</ol>

CC BY-SA 3.0
2014-05-27T09:38:20.913Z
Forgot that generalized arrows include primitives for $+$ type too. It seems that I need a kind of primitive recursion and minimization operators to make $\kappa$-calculus Turing-complete again. Thank you for the great answer.
polkovnikov.ph
CC BY-SA 3.0
2014-05-27T09:19:06.153Z
2014-05-27T10:24:19.600Z
2014-05-27T10:24:19.600Z
Neel Krishnaswami
<p>Suppose we have a <a href="https://en.wikipedia.org/wiki/Kappa_calculus" rel="nofollow noreferrer"><span class="math-container">$\kappa$</span>-calculus</a> with operator <span class="math-container">$fix$</span>, that could be used to transform function with type <span class="math-container">$(1 \rightarrow a) \rightarrow a$</span> to a value of type <span class="math-container">$1 \rightarrow a$</span>. We use a normal reduction strategy.</p>
<p>We'd like to represent factorial function in such a system. The problem is that whatever function we're trying to find a fixed point of, when we apply the function to its fixpoint, there's no way to determine whether we need to use the value of argument <span class="math-container">$x$</span> or not. There's no &quot;counter&quot; to base our solution on.</p>
<p><span class="math-container">$fix (\kappa{}x. \cdots) = (\kappa{}x. \cdots) (fix (\kappa{}x. \cdots))$</span></p>
<p>In <span class="math-container">$\lambda$</span>-calculus we could run <span class="math-container">$fix (\lambda f. \lambda x.\cdots)$</span> and terminate depending on the value of <span class="math-container">$x$</span>.</p>
<ol>
<li>How to prove that <span class="math-container">$\kappa$</span>-calculus with fixed point operator cannot really represent a factorial function?</li>
<li>How could we extend <span class="math-container">$\kappa$</span>-calculus to make it Turing-complete, leaving space for its translation into <a href="http://www.megacz.com/berkeley/garrows/" rel="nofollow noreferrer">generalized arrows</a>?</li>
</ol>

CC BY-SA 4.0
2020-04-26T23:22:10.890Z
Forgot to update with conclusions: there is a "loop over sum" operation in arrows, which is covered in literature not that well (in comparison to ["loop over product"](https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Arrow.html#v:loop)). It's required to define factorial.
polkovnikov.ph
<lo.logic><type-theory><lambda-calculus>
Can factorial be encoded in the Kappa-calculus with fixed point operator?
polkovnikov.ph
# Can factorial be encoded in the Kappa-calculus with fixed point operator?

(Asked by: username_0 on 2014-05-26)

Suppose we have a [$\kappa$-calculus](https://en.wikipedia.org/wiki/Kappa_calculus) with operator $fix$, that could be used to transform function with type $(1 \rightarrow a) \rightarrow a$ to a value of type $1 \rightarrow a$. We use a normal reduction strategy.

We'd like to represent factorial function in such a system. The problem is that whatever function we're trying to find a fixed point of, when we apply the function to its fixpoint, there's no way to determine whether we need to use the value of argument $x$ or not. There's no "counter" to base our solution on.

$fix (\kappa{}x. \cdots) = (\kappa{}x. \cdots) (fix (\kappa{}x. \cdots))$

In $\lambda$-calculus we could run $fix (\lambda f. \lambda x.\cdots)$ and terminate depending on the value of $x$.

1. How to prove that $\kappa$-calculus with fixed point operator cannot really represent a factorial function?
2. How could we extend $\kappa$-calculus to make it Turing-complete, leaving space for its translation into [generalized arrows](http://www.megacz.com/berkeley/garrows/)?

**Tags:** lo.logic, type-theory, lambda-calculus

> **Comments:**
> **username_0**: Forgot to update with conclusions: there is a "loop over sum" operation in arrows, which is covered in literature not that well (in comparison to ["loop over product"](https://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Arrow.html#v:loop)). It's required to define factorial.  

---

## 2 answers

### Answer by username_2 on 2014-05-27. Score: 11 | Accepted answer

The bare $\kappa$-calculus does not permit defining factorial, even when extended with a fixed point operator. However, this answer deserves some unpacking.

1. The fixed point operator you give is not well-formed according to the grammar of types in the $\kappa$-calculus. Note that the grammar of types does not contain the function space $\tau \Rightarrow \tau'$ -- this is because the $\kappa$-calculus is a language of *first-order* functions. An expression has a type $\tau\_1 \to \tau\_2$, to indicate that it is an expression of type $\tau\_2$, whose free variables are typed by $\tau\_1$.

   The proper typing for a fixed point operator would be roughly something like:
   $$
   \frac{\Gamma, x:1 \to \tau \vdash e : 1 \to \tau}
   {\Gamma \vdash \mu x:1 \to \tau. e : 1 \to \tau}
   $$
2. Once you've fixed this, you still can't define a factorial.

   The plain $\kappa$-calculus does not have sums or natural numbers as a base type. As a result, you can't write branching programs, and so you cannot define interesting recursive functions. If you added natural numbers and their iterator, you could define a factorial function. Hasegawa actually gives factorial as an example in his paper on the $\kappa$-calculus, in a calculus augmented with a basic natural number type.

   However, you might wonder why you *are* able to define factorial in the pure lambda calculus, even though it has no apparent control structures. The reason is that the interaction of fixed points and recursion gives you a "universal type" (i.e., a type $V$ such that $V$ is isomorphic to $V \to V$), and this lets you encode any datatype as a subset (more accurately, a retract) of it.

   In more syntactic terms, you can write the Y combinator (i.e., Curry's paradox) in any language with (a) higher-order functions, (b) recursion, and (c) the ability to use each variable more than once in a program. Since the basic $\kappa$-calculus lacks (a), adding even an unrestricted fixed point operator does not make it Turing-complete!

> **Comments:**
> **username_0**: Forgot that generalized arrows include primitives for $+$ type too. It seems that I need a kind of primitive recursion and minimization operators to make $\kappa$-calculus Turing-complete again. Thank you for the great answer.  

---

### Answer by username_1 on 2020-12-16. Score: 2

Not good with proofs but can answer number 2.
First of all it isn't necessary to use a complicated compilation scheme, you can just use PHOAS or a tagless final style directly.
class Category k => Terminal k where
     bang :: k a ()
class Terminal k => Kappa k where
     kappa :: (k () a -> k b c) -> k (a, b) c
     lift :: k () a -> k b (a, b)

I literally find this nowhere but there's a dual zeta calculus that composed with the Kappa calculus gives you a full lambda calculus
http://www.kurims.kyoto-u.ac.jp/~hassei/papers/ctcs95.html
class Terminal k => Zeta k where
    zeta :: (k () a -> k b c) -> k b (a -> c)
    pass :: k () a -> k (a -> b) b

class (Kappa k, Zeta k) => Lambda k

The dual constructions are literally just the same things but in the opposite category
class Category k => Initial k where
    absurd :: k Void a
class Initial k => Sum k where
     label :: (k a Void -> k c b) -> k c (a + b)
     jump :: k a Void -> k (a + b) b
class Initial k => Coexponential k where
     cozeta :: (k a Void -> k b c) -> k (b -< c) a
     compass :: k a Void -> k b (a -< b)
class (Sum K, Coexponential k) => Colambda k


would be a type synonym for Either probably. -< would have to be a phantom type

You would want to add Sum into the mix but not Coexponential which is basically just as powerful as exponentials but just really really strange.
Incidentally, you can't exactly really usefully have both exponentials and coexponentials in a programming language unless you have some sort of linear type system or something, not sure of the precise details.
Sum + Kappa is still not Turing complete IIRC.
If you had a Fixpoint type that is equivalent in power to a Fixpoint operater IIRC.
But I'm not sure that works without exponentials.


---

