Short demo of a lambda calculus curiosity, from Mirai Ikebuchi, Keisuke Nakano "On repetitive right application of B-terms" 2018

rho-property

{-# LANGUAGE OverloadedStrings #-}

import qualified Data.Set as S
import Data.String
import Data.List

type Var = String
data Expr = V Var | Ap Expr Expr | Lambda Var Expr
  deriving Eq

instance IsString Expr where
 fromString = V
λ = Lambda

instance Show Expr where
  show (V x) = x
  show (Ap f x) = '(' : show f ++ show x ++ ")"
  show (Lambda v e) = case show e of
    '(':'λ':s -> "(λ" ++ v ++ s
    r         -> "(λ" ++ v ++ "." ++ r ++ ")"

free :: Expr -> S.Set Var
free (V x) = S.singleton x
free (Lambda v e) = free e `S.difference` S.singleton v
free (Ap f e) = free f `S.union` free e

alpha :: Var -> Var -> Expr -> Expr
alpha x = subst x . V

subst :: Var -> Expr -> Expr -> Expr
subst v e' = go
 where
  go (V v') | v == v'   = e'
            | otherwise = V v'
  go (Ap f e) = Ap (go f) (go e)
  go (Lambda x e) | x == v              = Lambda x e
                  | x `notElem` free e' = Lambda x (go e)
                  | otherwise           = let y = fresh (Ap e e')
                                          in Lambda y (go (alpha x y e))

usedVars :: Expr -> [Var]
usedVars (V x) = [x]
usedVars (Ap f e) = usedVars f ++ usedVars e
usedVars (Lambda y e) = y:usedVars e

allVars :: [Var]
allVars = (map return "fghabcdevw") ++ ["v_" ++ show i | i <- [0..]]

fresh :: Expr -> Var
fresh = head . (allVars \\) . usedVars

normal :: Expr -> Bool
normal (V x) = True
normal (Ap Lambda{} _) = False
normal (Ap f x) = normal f && normal x
normal (Lambda x e) = normal e

beta :: Expr -> Expr
beta (V x) = V x
beta (Lambda x e) = Lambda x (beta e)
beta (Ap (Lambda x e) e') = subst x e' e
beta (Ap (V r) e) = Ap (V r) (beta e)
beta (Ap f e) = if normal f then Ap f (beta e)
                else Ap (beta f) e

beta' :: Expr -> Expr
beta' = until normal beta

-- This assumes terms are both beta and eta normalized.
alphaEq :: Expr -> Expr -> Bool
alphaEq (V x) (V y) = x == y
alphaEq (Lambda x e) (Lambda y f) = alpha y x f `alphaEq` e
alphaEq (Ap f e) (Ap g e') = f `alphaEq` g && e `alphaEq` e'
alphaEq _ _ = False

lid = λ"x" "x"
ldot = λ"g" (λ"f" (λ"x" (Ap "g" (Ap "f" "x"))))
lflip = λ"f" (λ"x" (λ"y" (Ap (Ap "f" "y") "x")))

power 1 x = x
power n x = power (n - 1) x `Ap` x

test e n m = do
  let left = beta' (power n e)
      right = beta' (power m e)
  putStrLn (show e ++ "^" ++ show n ++ " = " ++ show left)
  putStrLn (show e ++ "^" ++ show m ++ " = " ++ show right)
  print (left `alphaEq` right)
  
main = do
  test lid 1 2
  test lflip 3 4
  -- Note ldot is fmap for the Hom(a, _) functor.
  test ldot 6 10