Last active
October 21, 2022 02:24
-
-
Save friedbrice/80ec47a847eaa5bf670c85632e3da804 to your computer and use it in GitHub Desktop.
Looking for a Needle That Might Not Be in an Infinite Haystack
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- Based on "Infinite sets that admit fast exhaustive search" by Martín Escardó | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| {-# LANGUAGE MultiWayIf #-} | |
| module Escardo where | |
| import Prelude hiding (Real) | |
| import Data.Bool | |
| import Numeric.Natural | |
| instance Num Bool where | |
| p + q = p && not q || not p && q | |
| p * q = p && q | |
| negate p = p | |
| abs p = p | |
| signum p = 1 | |
| fromInteger = not . even | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| type Quantifier a = (a -> Bool) -> Bool | |
| type Searcher a = (a -> Bool) -> a | |
| class Searchable a where | |
| -- Law: | |
| -- if at least one member of `a` satisfies `p` | |
| -- then `p (query p) = True`. | |
| query :: Searcher a | |
| search :: Searchable a => (a -> Bool) -> Maybe a | |
| search p = | |
| case query p of | |
| x | p x -> Just x | |
| | otherwise -> Nothing | |
| exists :: Searchable a => Quantifier a | |
| exists = not . null . search | |
| forAll :: Searchable a => Quantifier a | |
| forAll p = (not . exists) (not . p) | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| instance Searchable Bool where | |
| -- case 1) | |
| -- if p True = True | |
| -- then p (query p) = p (p True) = p True = True | |
| -- | |
| -- case 2) | |
| -- if p True = False && p False = True | |
| -- then p (query p) = p (p True) = p False = True | |
| -- | |
| -- case 3) | |
| -- if p True = False && p False = False | |
| -- then p (query p) = p (p True) = False = False | |
| query p = p True | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| instance (Searchable a, Searchable b) => | |
| Searchable (a, b) where | |
| query p = (a0, b0) | |
| where | |
| a0 = query (\a -> exists (\b -> p ( a, b))) | |
| b0 = query (\b -> p (a0, b) ) | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| type Sequence a = Natural -> a | |
| instance Searchable a => Searchable (Sequence a) where | |
| query = tychonoff (const query) | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| data Tree a = Branch a (Tree a) (Tree a) | |
| tychonoff :: forall a. | |
| Sequence (Searcher a) -> Searcher (Sequence a) | |
| tychonoff searchers cond = res | |
| where | |
| res :: Sequence a | |
| res = decode . encode $ \i -> | |
| searchers i $ \a -> | |
| rev a i $ | |
| tychonoff | |
| (\i' -> searchers (i' + i + 1)) | |
| (rev a i) | |
| rev :: a -> Natural -> Sequence a -> Bool | |
| rev a i as = | |
| cond $ \i' -> if | i' < i -> res i' | |
| | i' == i -> a | |
| | otherwise -> as (i' - i - 1) | |
| encode :: Sequence a -> Tree a | |
| encode f = | |
| Branch (f 0) (encode (\n -> f (2 * n + 1))) | |
| (encode (\n -> f (2 * n + 2))) | |
| decode :: Tree a -> Sequence a | |
| decode (Branch x l r) n = | |
| case n of | |
| 0 -> x | |
| n | odd n -> decode l ((n - 1) `div` 2) | |
| | otherwise -> decode r ((n - 2) `div` 2) | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| type Real = Sequence Bool | |
| f :: Real -> Integer | |
| f x = | |
| x' | |
| $ 10 * x' (3 ^ 80) | |
| + 100 * x' (4 ^ 80) | |
| + 1000 * x' (5 ^ 80) | |
| where | |
| x' = ints x | |
| g :: Real -> Integer | |
| g x = | |
| x' | |
| $ 10 * x' (3 ^ 80) | |
| + 100 * x' (4 ^ 80) | |
| + 1000 * x' (6 ^ 80) | |
| where | |
| x' = ints x | |
| h :: Real -> Integer | |
| h x = | |
| if x' (4 ^ 80) == 0 | |
| then x' j | |
| else x' (100 + j) | |
| where | |
| i = if x' (5 ^ 80) == 0 then 0 else 1000 | |
| j = if x' (3 ^ 80) == 1 then 10 + i else i | |
| x' = ints x | |
| ints :: Sequence Bool -> Integer -> Integer | |
| ints x = bool 0 1 . x . fromIntegral | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| instance (Searchable a, Eq b) => Eq (a -> b) where | |
| f == g = forAll (\a -> f a == g a) | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- | |
| -- |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment