In this post, we will restrict our attention to finite functions. For finite functions, we already know how to decide injectivity and surjectivity. Hence, deciding the bijectivity of finite functions is now trivial. In Haskell, we create the following three predicates:
isInjective :: (Eq a, Eq b) => (a -> b) -> [a] -> Bool isInjective f xs = all phi [(x1,x2) | x1 <- xs, x2 <- xs] where phi (x1,x2) = (f x1 /= f x2) || (x1 == x2) isSurjective :: Eq b => (a -> b) -> [a] -> [b] -> Bool isSurjective f xs ys = all psi ys where psi y = or [(f x == y) | x <- xs] isBijective :: (Eq a, Eq b) => (a -> b) -> [a] -> [b] -> Bool isBijective f xs ys = (isInjective f xs) && (isSurjective f xs ys)
Note that predicate isInjective takes as inputs a function and a list (the domain), whereas predicate isSurjective takes as inputs a function and two lists (the domain and the codomain). Both return either True or False. Predicate isBijective is defined using the conjunction of the other two predicates. In this implementation, we separated the decision procedure from the definition of .
Let us define . Consider the finite function
*Main> let f n = (3 * n) `mod` 4 *Main> isInjective f [0..3] True *Main> isSurjective f [0..3] [0..3] True *Main> isBijective f [0..3] [0..3] True
Consider now the following finite function
We already know that function is neither injective nor surjective. Hence, it is not bijective. Here’s a GHCi session:
*Main> let g n = (2 * n) `mod` 4 *Main> isInjective g [0..3] False *Main> isSurjective g [0..3] [0..3] False *Main> isBijective g [0..3] [0..3] False