Advertisement
Guest User

infinite-search

a guest
Mar 16th, 2012
111
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Python 6.03 KB | None | 0 0
  1. #!/usr/bin/env python
  2.  
  3.  
  4. # -- File "seemingly-impossible.hs",
  5. # -- automatically extracted from literate Haskell
  6. # -- file http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html
  7. # --
  8. # -- Martin Escardo, September 2007
  9. # -- School of Computer Science, University of Birmingham, UK
  10. # --
  11. # -- These algorithms have been published and hence are in the
  12. # -- public domain.
  13. # --
  14. # -- If you use them, I'd like to know! mailto:m.escardo@cs.bham.ac.uk
  15. #
  16. # infix hack:
  17. # https://code.activestate.com/recipes/384122/
  18. class Infix:
  19.     def __init__(self, function):
  20.         self.function = function
  21.     def __ror__(self, other):
  22.         return Infix(lambda x, self=self, other=other: self.function(other,
  23. x))
  24.     def __or__(self, other):
  25.         return self.function(other)
  26.     def __rlshift__(self, other):
  27.         return Infix(lambda x, self=self, other=other: self.function(other,
  28. x))
  29.     def __rshift__(self, other):
  30.         return self.function(other)
  31.     def __call__(self, value1, value2):
  32.         return self.function(value1, value2)
  33.  
  34.  
  35. def ifthen(test, trueF, falseF):
  36.  if (test):
  37.    return trueF()
  38.  else:
  39.    return falseF()
  40.  
  41. # data Bit = Zero | One
  42. #          deriving (Eq)
  43.  
  44. # Don't bother with a dedicated type or coerce, just define some constants
  45. zero = 0
  46. one = 1
  47.  
  48.  
  49. # type Natural = Integer
  50. # type Cantor = Natural -> Bit
  51. # (#) :: Bit -> Cantor -> Cantor
  52.  
  53. # x # a = lambda i: if i == 0 then x else a(i-1)
  54. q = Infix ( lambda x, a: (lambda i: ifThen ((i ==0), (lambda: x), (lambda: a(i-1)))))
  55.  
  56. # forsome, forevery :: (Cantor -> Bool) -> Bool
  57. # find :: (Cantor -> Bool) -> Cantor
  58. # find = find_i
  59. find = lambda p: find_i(p)
  60.  
  61. # find_i :: (Cantor -> Bool) -> Cantor
  62. # find_i p = if forsome(lambda a: p(Zero # a))
  63. #            then Zero # find_i(lambda a: p(Zero # a))
  64. #            else One  # find_i(lambda a: p(One  # a))
  65. # search :: (Cantor -> Bool) -> Maybe Cantor
  66.  
  67. # forevery p = not(forsome(lambda a: not(p a)))
  68. def forevery(p): not (forsome( lambda a: not (p (a))))
  69.  
  70. # forsome p = p(find(lambda a: p(a)))
  71. def forsome(p): p(find_i(lambda a: p(a)))
  72.  
  73. def find_i (p):
  74.   if forsome (lambda a: p(zero |q| a)):
  75.     return zero |q| find_i(lambda a: p( zero |q| a))  
  76.   else:
  77.     return one  |q| find_i(lambda a: p( one  |q| a))  
  78.  
  79. # search p = if forsome(lambda a: p(a)) then Just(find(lambda a: p(a))) else Nothing
  80. def search (p):
  81.  if forsome(lambda a : p(a)):
  82.    find(lambda a: p(a))
  83.  else: None
  84.  
  85. # equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
  86. # equal f g = forevery(lambda a: f(a) == g(a))
  87. def equal(f, g): forevery(lambda a: f(a) == g(a))
  88.  
  89. # coerce :: Bit -> Natural
  90. # coerce Zero = 0
  91. # coerce One = 1
  92. coerce = lambda x: x
  93.  
  94. # f, g, h :: Cantor -> Integer
  95. f = lambda a: coerce(a(7 * coerce(a(4)) +  4 * (coerce(a(7))) + 4))
  96. g = lambda a: coerce(a(coerce(a(4)) + 11 * (coerce(a(7)))))
  97. def h(a):
  98.       if a(7) == zero:
  99.         if a(4) == zero:
  100.            coerce(a(4))
  101.         else:
  102.            coerce(a( 11))
  103.       else:
  104.            if a(4) == one:
  105.              coerce(a( 15) )
  106.            else:
  107.              coerce(a(8))
  108.  
  109. # modulus :: (Cantor -> Integer) -> Natural
  110. # FIXME
  111. def modulus (f):  least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b)))))
  112.  
  113. # least :: (Natural -> Bool) -> Natural
  114. def least (p):
  115.   if p(0):
  116.    x=0
  117.   else:
  118.    x=1
  119.   x + least(lambda n: p(n+1))
  120.  
  121. # eq :: Natural -> Cantor -> Cantor -> Bool
  122. def eq (n,a,b):
  123.   if (n == 0):
  124.     return True
  125.   else:
  126.    return (a(n-1) == b (n-1)) and (eq(n,a,b))
  127.  
  128. # proj :: Natural -> (Cantor -> Integer)
  129. def proj(i): lambda a: coerce(a(i))
  130.  
  131.  
  132. # find_ii p = if p(Zero # find_ii(lambda a: p(Zero # a)))
  133. #             then Zero # find_ii(lambda a: p(Zero # a))
  134. #             else One  # find_ii(lambda a: p(One  # a))
  135. # find_iii :: (Cantor -> Bool) -> Cantor
  136. # find_iii p = h # find_iii(lambda a: p(h # a))
  137. #        where h = if p(Zero # find_iii(lambda a: p(Zero # a))) then Zero else
  138. #        One
  139. # find_iv :: (Cantor -> Bool) -> Cantor
  140. # find_iv p = let leftbranch = Zero # find_iv(lambda a: p(Zero # a))
  141. #             in if p(leftbranch)
  142. #                then leftbranch
  143. #                else One # find_iv(lambda a: p(One # a))
  144. # find_v :: (Cantor -> Bool) -> Cantor
  145. # find_v p = lambda n:  if q n (find_v(q n)) then Zero else One
  146. #  where q n a = p(lambda i: if i < n then find_v p i else if i == n then Zero
  147. #  else a(i-n-1))
  148. # find_vi :: (Cantor -> Bool) -> Cantor
  149. # find_vi p = b
  150. #  where b = lambda n: if q n (find_vi(q n)) then Zero else One
  151. #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
  152. #        a(i-n-1))
  153. # find_vii :: (Cantor -> Bool) -> Cantor
  154. # find_vii p = b
  155. #  where b = id'(lambda n: if q n (find_vii(q n)) then Zero else One)
  156. #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
  157. #        a(i-n-1))
  158.  
  159. # data T x = B x (T x) (T x)
  160. # code :: (Natural -> x) -> T x
  161. # code f = B (f 0) (code(lambda n: f(2*n+1)))
  162. #                  (code(lambda n: f(2*n+2)))
  163. # decode :: T x -> (Natural -> x)
  164. # decode (B x l r) n |  n == 0    = x
  165. #                    |  odd n     = decode l ((n-1) `div` 2)
  166. #                    |  otherwise = decode r ((n-2) `div` 2)
  167. # id' :: (Natural -> x) -> (Natural -> x)
  168. # id' = decode.code
  169. # f',g',h' :: Cantor -> Integer
  170. # f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce(a
  171. # i)
  172. # g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce(a
  173. # i)
  174. # h' a = a' k
  175. #     where i = if a'(5^80) == 0 then 0    else 1000
  176. #           j = if a'(3^80) == 1 then 10+i else i
  177. #           k = if a'(4^80) == 0 then j    else 100+j
  178. #           a' i = coerce(a i)
  179.  
  180. # pointwiseand :: [Natural] -> (Cantor -> Bool)
  181. # pointwiseand [] = lambda b: True
  182. # FIXME how to emulate pattern match (n:a)
  183. def  pointwiseand (ns):
  184.   if (ns == []):
  185.     return True
  186.   else:
  187.     return (lambda b: (b(ns[0]) == one) and pointwiseand(ns[0], b))
  188.  
  189. # sameelements :: [Natural] -> [Natural] -> Bool
  190. sameelements = lambda a, b:  equal (pointwiseand(a), pointwiseand(b))
  191.  
  192. equal(f,g)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement