0
$\begingroup$

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

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.