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