Advertisement
Guest User

the impossible fixed

a guest
Mar 17th, 2012
87
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  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. def q(x,a): return (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.  
  60. # find_i :: (Cantor -> Bool) -> Cantor
  61. # find_i p = if forsome(lambda a: p(Zero # a))
  62. #            then Zero # find_i(lambda a: p(Zero # a))
  63. #            else One  # find_i(lambda a: p(One  # a))
  64. # search :: (Cantor -> Bool) -> Maybe Cantor
  65.  
  66. # forevery p = not(forsome(lambda a: not(p a)))
  67. def forevery(p): return (not (forsome( lambda a: not (p (a)))))
  68.  
  69. # forsome p = p(find(lambda a: p(a)))
  70. def forsome(p): return (p(find_ii(lambda a: p(a))))
  71.  
  72. def find_ii(p): return (lambda j: ifthen (p(q (zero, find_ii (lambda a: p(q(zero, a)))))
  73.          ,lambda : q(zero, find_ii(lambda a: p(q(zero, a))))(j)
  74.          ,lambda : q(one, find_ii(lambda a: p(q(one, a))))(j)))
  75.  
  76. # search p = if forsome(lambda a: p(a)) then Just(find(lambda a: p(a))) else Nothing
  77. def search (p):
  78.  if forsome(lambda a : p(a)):
  79.    find(lambda a: p(a))
  80.  else: None
  81.  
  82. # equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
  83. # equal f g = forevery(lambda a: f(a) == g(a))
  84. def equal(f, g): return (forevery(lambda a: f(a) == g(a)))
  85.  
  86. # coerce :: Bit -> Natural
  87. # coerce Zero = 0
  88. # coerce One = 1
  89. coerce = lambda x: x
  90.  
  91. # f, g, h :: Cantor -> Integer
  92. f = lambda a: coerce(a(2 * coerce(a(4)) +  4 * (coerce(a(5)))))
  93. g = lambda a: coerce(a(coerce(a(4)) + 4 * (coerce(a(5)))))
  94. def h(a):
  95.       if a(5) == zero:
  96.         if a(4) == zero:
  97.            return (coerce(a(0)))
  98.         else:
  99.            return (coerce(a(2)))
  100.       else:
  101.            if a(4) == one:
  102.              return (coerce(a(6) ))
  103.            else:
  104.              return (coerce(a(4)))
  105.  
  106. # modulus :: (Cantor -> Integer) -> Natural
  107. # FIXME
  108. def modulus (f): return (least(lambda n: forevery(lambda a: forevery(lambda b: (not (eq(n, a, b))) or (f(a) == f( b))))))
  109.  
  110. # least :: (Natural -> Bool) -> Natural
  111. def least (p):
  112.   if p(0):
  113.    return 0
  114.   else:
  115.    return (1 + least(lambda n: p(n+1)))
  116.  
  117. # eq :: Natural -> Cantor -> Cantor -> Bool
  118. def eq (n,a,b):
  119.   if (n == 0):
  120.     return True
  121.   else:
  122.    return (a(n-1) == b (n-1)) and (eq(n-1,a,b))
  123.  
  124. # proj :: Natural -> (Cantor -> Integer)
  125. def proj(i): return (lambda a: coerce(a(i)))
  126.  
  127.  
  128. # find_ii p = if p(Zero # find_ii(lambda a: p(Zero # a)))
  129. #             then Zero # find_ii(lambda a: p(Zero # a))
  130. #             else One  # find_ii(lambda a: p(One  # a))
  131. # find_iii :: (Cantor -> Bool) -> Cantor
  132. # find_iii p = h # find_iii(lambda a: p(h # a))
  133. #        where h = if p(Zero # find_iii(lambda a: p(Zero # a))) then Zero else
  134. #        One
  135. # find_iv :: (Cantor -> Bool) -> Cantor
  136. # find_iv p = let leftbranch = Zero # find_iv(lambda a: p(Zero # a))
  137. #             in if p(leftbranch)
  138. #                then leftbranch
  139. #                else One # find_iv(lambda a: p(One # a))
  140. # find_v :: (Cantor -> Bool) -> Cantor
  141. # find_v p = lambda n:  if q n (find_v(q n)) then Zero else One
  142. #  where q n a = p(lambda i: if i < n then find_v p i else if i == n then Zero
  143. #  else a(i-n-1))
  144. # find_vi :: (Cantor -> Bool) -> Cantor
  145. # find_vi p = b
  146. #  where b = lambda n: if q n (find_vi(q n)) then Zero else One
  147. #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
  148. #        a(i-n-1))
  149. # find_vii :: (Cantor -> Bool) -> Cantor
  150. # find_vii p = b
  151. #  where b = id'(lambda n: if q n (find_vii(q n)) then Zero else One)
  152. #        q n a = p(lambda i: if i < n then b i else if i == n then Zero else
  153. #        a(i-n-1))
  154.  
  155. # data T x = B x (T x) (T x)
  156. # code :: (Natural -> x) -> T x
  157. # code f = B (f 0) (code(lambda n: f(2*n+1)))
  158. #                  (code(lambda n: f(2*n+2)))
  159. # decode :: T x -> (Natural -> x)
  160. # decode (B x l r) n |  n == 0    = x
  161. #                    |  odd n     = decode l ((n-1) `div` 2)
  162. #                    |  otherwise = decode r ((n-2) `div` 2)
  163. # id' :: (Natural -> x) -> (Natural -> x)
  164. # id' = decode.code
  165. # f',g',h' :: Cantor -> Integer
  166. # f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce(a
  167. # i)
  168. # g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce(a
  169. # i)
  170. # h' a = a' k
  171. #     where i = if a'(5^80) == 0 then 0    else 1000
  172. #           j = if a'(3^80) == 1 then 10+i else i
  173. #           k = if a'(4^80) == 0 then j    else 100+j
  174. #           a' i = coerce(a i)
  175.  
  176. # pointwiseand :: [Natural] -> (Cantor -> Bool)
  177. # pointwiseand [] = lambda b: True
  178. # FIXME how to emulate pattern match (n:a)
  179. def  pointwiseand (ns):
  180.   if (ns == []):
  181.     return True
  182.   else:
  183.     return (lambda b: (b(ns[0]) == one) and pointwiseand(ns[0], b))
  184.  
  185. # sameelements :: [Natural] -> [Natural] -> Bool
  186. sameelements = lambda a, b:  equal (pointwiseand(a), pointwiseand(b))
  187.  
  188. print modulus(proj(1))
  189. print equal(h,h)
  190. print equal(h,g)
  191. print equal(h,f)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement