where and range over set . We now introduce the injectivity predicate , defined by
so that function is injective if and only if is true. In this post we will restrict our attention to finite functions, for which it is fairly straightforward to devise a decision procedure to decide injectivity. Let denote the cardinality of set . Then, determining the truth value of will require a total of evaluations of the predicate .
Let us define . Consider the finite function
where denotes modulo 4 arithmetic. Is injective? Note that , , , and . Hence, we easily conclude that is injective. Suppose that we do not want to enumerate the images of the elements of under ; in that case, we can use the following Haskell script to decide that is injective:
-- define function f f :: Integral a => a -> a f n = (3 * n) `mod` 4 -- define disjunction (\/) :: Bool -> Bool -> Bool p \/ q = p || q -- define implication (==>) :: Bool -> Bool -> Bool p ==> q = (not p) \/ q -- define injectivity predicate phi :: Integral a => (a,a) -> Bool phi (x1,x2) = (f x1 == f x2) ==> (x1 == x2)
where we used the fact that is semantically equivalent to . Let us carry out some testing:
*Main> -- test function f *Main> [ f n | n <- [0..3]] [0,3,2,1] *Main> -- test disjunction *Main> [ p \/ q | p <-[True, False], q <- [True, False]] [True,True,True,False] *Main> -- test implication *Main> [ p ==> q | p <-[True, False], q <- [True, False]] [True,False,True,True]
So far, so good. Finally, we can determine the truth value of the sentence using function all, as follows:
*Main> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]] True
which allows us to conclude that is injective.
An alternative procedure would be to use function nub from library Data.List to remove duplicates from a given list. Note that is injective if and only if the list of the images of the elements of under contains no duplicates. Hence, we obtain:
*Main> let images = [ f n | n <- [0..3]] *Main> import Data.List *Main Data.List> length (nub images) == length images True
What a hack! This second procedure might seem much terser than the first one. But if we do away with type declarations and refrain from re-defining disjunction and defining implication, the first procedure can be made quite succinct as well:
Prelude> let f n = (3 * n) `mod` 4 Prelude> let phi (x1,x2) = not (f x1 == f x2) || (x1 == x2) Prelude> all phi [(x1,x2) | x1 <- [0..3], x2 <- [0..3]] True
which includes the definition of function . Three lines only! Three!