You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
56 lines
1.7 KiB
56 lines
1.7 KiB
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}
|
|
|
|
import Control.Monad.Instances
|
|
import Coalgebra
|
|
import Search
|
|
|
|
-- F X = 1 + X
|
|
type F = Maybe
|
|
|
|
-- This will give the fixpoint, ie a coalgebra, because F is a functor
|
|
-- There is an element for every natural number, and an infinity element
|
|
type Natinfi = Nu F
|
|
|
|
-- The semantics from the following coalgebra to Natinfi is "the selection function"
|
|
-- In some sense this behaviour searches through all natural numbers
|
|
-- (searching for a witness x such that p x = True, in contrast to the paper)
|
|
instance Coalgebra F (Natinfi -> Bool) where
|
|
psi p
|
|
| p (phi Nothing) == True = Nothing
|
|
| otherwise = Just (\x -> p $ phi $ Just x)
|
|
|
|
-- http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ says:
|
|
-- "What is going on here is that computable functionals are continuous"
|
|
-- In this case Natinfi is compact, so any computable predicate is known when we only inverstigate at depth n (for some n)
|
|
-- Hence forsome and others will always terminate.
|
|
test1 :: Natinfi -> Bool
|
|
test1 p = case q of
|
|
Nothing -> False
|
|
Just y -> True
|
|
where q = psi p
|
|
|
|
test2 :: Natinfi -> Bool
|
|
test2 p = case q of
|
|
Nothing -> False
|
|
Just y -> False
|
|
where q = psi p
|
|
|
|
-- Of course this will not always terminate!
|
|
toInt :: Natinfi -> Int
|
|
toInt s = case q of
|
|
Nothing -> 0
|
|
Just y -> 1 + toInt y
|
|
where q = psi s
|
|
|
|
sNatinfi :: Searchable Natinfi
|
|
sNatinfi = S (semantics :: (Natinfi -> Bool) -> Natinfi)
|
|
|
|
output :: (Natinfi -> Bool) -> String
|
|
output p
|
|
| forsome sNatinfi p == True = "There is an example, namely: " ++ (show $ toInt $ find sNatinfi p)
|
|
| otherwise = "For all elements p is false"
|
|
|
|
main :: IO ()
|
|
main = do
|
|
putStrLn $ output test1
|
|
putStrLn $ output test2
|