{-|
Module: Ski
Description: Ski expressions and bracket abstraction.
License: GPL-3
This module implements a representation of the SKI subset of the
calculus of combinators. It provides a lambda abstraction algorithm
writing lambda expressions as combinators.
-}
module Ski
( Ski (S, K, I, Comb)
, skiabs
)
where
import NamedLambda
-- | A SKI combinator expression
data Ski = S | K | I | Comb Ski Ski | Cte String
deriving (Eq, Ord)
instance Show Ski where
show = showski
-- | Shows a SKI expression
showski :: Ski -> String
showski S = "S"
showski K = "K"
showski I = "I"
showski (Cte _) = "?"
showski (Comb x S) = showski x ++ showski S
showski (Comb x K) = showski x ++ showski K
showski (Comb x I) = showski x ++ showski I
showski (Comb x (Cte c)) = showski x ++ showski (Cte c)
showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")"
-- | SKI abstraction of a named lambda term. From a lambda expression
-- creates a SKI equivalent expression. The following algorithm is a
-- version of the algorithm 9.10 on the Hindley-Seldin book.
skiabs :: NamedLambda -> Ski
skiabs (LambdaVariable x) = Cte x
skiabs (LambdaApplication m n) = Comb (skiabs m) (skiabs n)
skiabs (LambdaAbstraction x m) = bracketabs x (skiabs m)
-- | Bracket abstraction of a SKI term, as defined in Hindley-Seldin
-- (2.18).
bracketabs :: String -> Ski -> Ski
bracketabs _ S = Comb K S
bracketabs _ K = Comb K K
bracketabs _ I = Comb K I
bracketabs x (Cte y) = if x == y then I else Comb K (Cte y)
bracketabs x (Comb u (Cte y))
| freein x u && x == y = u
| freein x u = Comb K (Comb u (Cte y))
| otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x (Cte y))
bracketabs x (Comb u v)
| freein x (Comb u v) = Comb K (Comb u v)
| otherwise = Comb (Comb S (bracketabs x u)) (bracketabs x v)
-- | Checks if a given variable is used on a SKI expression.
freein :: String -> Ski -> Bool
freein _ S = True
freein _ K = True
freein _ I = True
freein x (Cte y) = not (x == y)
freein x (Comb u v) = freein x u && freein x v
-- -- | Bracket abstraction of a lambda term. The following algorithm is
-- -- an adaptation to deBruijn indexes of the definition 2.18 and 9.10
-- -- of the Hindley-Seldin book.
-- skiabs :: Exp -> Ski
-- -- Error, the formula is not a closed one
-- skiabs (Var n) = undefined
-- -- The first case is the identity
-- skiabs (Lambda (Var 1)) = I
-- -- Only if the variable is free
-- skiabs (Lambda (App u (Var 1)))
-- | freein 1 u = skiabs u
-- | otherwise = Comb (Comb S (skiabs u)) I
-- -- Combination
-- skiabs (Lambda m@(App u v))
-- | freein 1 m = Comb K (skiabs m)
-- | otherwise = Comb (Comb S (skiabs u)) (skiabs v)
-- -- Error on pattern matching
-- skiabs (Lambda e) = undefined
-- skiabs (App u v) = Comb (skiabs u) (skiabs v)