# Is having a particular form equivalent to being computable for functions on Church numerals?

In SKI-combinator calculus, consider the following function which reduces an expression (involving SKI and variables) to a canonical form:

fn canonical(expr):
if atomic expr: // S, K, I, or variable
expr
else if leftmost expr is a variable: // leftmost is the left-most atomic term
apply (canonical (left expr)) (canonical (right expr))
else:
build_lamda (canonical (apply expr new_var))

fn build_lambda(new_var -> expr):
case expr of
new_var -> I
x y -> case (build_lambda x, build_lambda y) of
(K x', K y') -> K (x' y')
(K x', I) -> x
(x', y') -> S x' y'
other -> K other // S, K, I, or other variable besides the new one


Note that if canonical halts on an expression E, then it will also halt on any expression E' which is extensionally equivalent to E and give the same result.

This is stronger than the guarantees made by putting an expression in normal form. Eg. SKK, S(KI), and I are all in normal form and are extensionally equivalent. However canonical S(KI) = canonical SKK = canonical I all evaluate to I.

Are there examples of a function in canonical form which operates on (any number of) Church numerals and does not halt on all (Church numeral) inputs?

Conversely, are there examples of a function which is computable which has no canonical form for Church numerals?

In other words, for functions on Church numerals, is having a canonical form equivalent to being computable?

I was hoping the pseudo-code above is clear, but in case it's not, here's the full Haskell code for canonical:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleInstances #-}

module Lib where

import Data.Void (Void, absurd)
import Prelude hiding ((*))

data Ski v
= S
| K
| I
| Var v
| Ski v :* Ski v
deriving (Functor)

infixl 9 :*

instance Show (Ski Void) where
showsPrec _ S = showString "S"
showsPrec _ K = showString "K"
showsPrec _ I = showString "I"
showsPrec _ (Var v) = absurd v
showsPrec d (x :* y) = showParen (d > 10) $showsPrec 10 x . showsPrec 11 y eval :: Ski v -> Ski v eval (x0 :* y0) = eval x0 * eval y0 eval atom = atom apply :: Ski v -> Ski v -> Ski v apply (S :* x :* y) z = x * z * (y * z) apply (K :* x) _y = x apply I x = x apply x y = x :* y (*) :: Ski v -> Ski v -> Ski v (*) = apply infixl 9 * data AddVar v = NewVar | OldVar v lamda :: Ski (AddVar v) -> Ski v lamda (Var NewVar) = I lamda (x0 :* y0) = case (lamda x0, lamda y0) of (K :* x, K :* y) -> K :* (x :* y) (K :* x, I) -> x (x, y) -> S :* x :* y lamda S = K :* S lamda K = K :* K lamda I = K :* I lamda (Var (OldVar x)) = K :* Var x lam :: (Ski (AddVar v) -> Ski (AddVar v)) -> Ski v lam f = lamda (f (Var NewVar)) leftmostIsVar :: Ski v -> Bool leftmostIsVar (Var _) = True leftmostIsVar (x :* _y) = leftmostIsVar x leftmostIsVar _ = False canonical :: Ski v -> Ski v canonical = go . eval where go :: Ski v -> Ski v go expr | leftmostIsVar expr = breakdown expr | otherwise = lam $$\v -> go$$ (OldVar <$> expr) * v
breakdown :: Ski v -> Ski v
breakdown (x :* y) = breakdown x :* go y
breakdown atom = atom


and here's some example usage (with a helper class to avoid explicitly lifting and unlifting between variable contexts)

{-# LANGUAGE MultiParamTypeClasses #-}

class VarInto v w where
var' :: v -> w

instance VarInto v v where
var' = id

instance {-# INCOHERENT #-} VarInto v w => VarInto v (AddVar w) where
var' = OldVar . var'

var :: VarInto v w => Ski v -> Ski w
var = fmap var'

compose :: Ski v
compose = lam $$\x -> lam$$ \y -> lam $\z -> var x :* (var y :* var z) flip1 :: Ski v flip1 = lam $$\x -> lam$$ \y -> lam$ \z ->
var x :* var z :* var y

flip2 :: Ski v
flip2 = flip1 * (compose * compose * S) * K

\$ ghci

> flip1 :: Ski Void
S(S(KS)(S(KK)S))(KK)
> flip2 :: Ski Void
S(S(K(S(KS)K))S)(KK)
> canonical flip2 :: Ski Void
S(S(KS)(S(KK)S))(KK)
> apply flip1 K :: Ski Void
S(K(SK))K
> canonical (apply flip1 K) :: Ski Void
KI