# a-conjecture-of-mine

An exercise on polyglossy: the same problem solved on multiple languages

```commit 3534aeddadee0b3403b2242781c56cda1fa711b9
parent f14206ab3fb8a764b7125c2613b2cf5687011d74
Author: Pablo Escobar Gaviria <gark.garcia@protonmail.com>
Date:   Mon, 13 Jan 2020 21:46:39 -0200

Formated the Wasm implementation.

Diffstat:
M.gitignore | 1+
MHaskell/Main.hs | 8++++----
AIdris/Data/Map.ibc | 0
AIdris/Data/Map.idr | 149+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
AIdris/Main.idr | 74++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
MREADME.md | 28+++++++++++++++++-----------
MWasm/main.wat | 121++++++++++++++++++++++++++++++++++++++++++++++++-------------------------------

7 files changed, 318 insertions(+), 63 deletions(-)
```
```diff --git a/.gitignore b/.gitignore
@@ -5,6 +5,7 @@
*.beam
bin
build
+*.un~
Statistics
Latex
Cuda
diff --git a/Haskell/Main.hs b/Haskell/Main.hs
@@ -17,9 +17,9 @@ main :: IO Int
main = do
args <- getArgs

-    case head' args >>= Just . readDec of
+    case readDec <\$> head' args of
Just [(max, "")] ->
-            if counter' max then exitFailure else exitSuccess
+            if counterexempl max then exitFailure else exitSuccess
_ -> exitInvalidInput

where head' [] = Nothing
@@ -66,8 +66,8 @@ diff sums (a, b) = do
--
-- Returns `True` if a counter example was found.
-- Otherwise returns `False`.
-counter' :: Natural -> Bool
-counter' max =
+counterexempl :: Natural -> Bool
+counterexempl max =
case foldM test' empty [(a, b) | a <- [0..max], b <- [a..max]] of
Nothing -> True
Just _  -> False
diff --git a/Idris/Data/Map.ibc b/Idris/Data/Map.ibc
Binary files differ.
diff --git a/Idris/Data/Map.idr b/Idris/Data/Map.idr
@@ -0,0 +1,149 @@
+module Data.Map
+
+public export
+data Map k a = Bin Nat k a (Map k a) (Map k a)
+             | Tip
+
+implementation Sized (Map k a) where
+  size (Bin s _ _ _ _) = s
+  size Tip = 0
+
+ratio : Nat
+ratio = 2
+
+delta : Nat
+delta = 3
+
+raise : String -> Map k v
+raise _ = ?undefined
+
+-- | /O(1)/. The empty map.
+public export
+empty : Map k a
+empty = Tip
+
+-- | /O(1)/. A map with a single element.
+--
+-- > singleton 1 'a'        == fromList [(1, 'a')]
+-- > size (singleton 1 'a') == 1
+public export
+singleton : k -> a -> Map k a
+singleton k x = Bin 1 k x Tip Tip
+
+-- balanceL is called when left subtree might have been inserted to or when
+-- right subtree might have been deleted from.
+balanceL : k -> a -> Map k a -> Map k a -> Map k a
+balanceL k x l r =
+  case r of
+    Tip =>
+      case l of
+        Tip => Bin 1 k x Tip Tip
+        (Bin _ _ _ Tip Tip) => Bin 2 k x l Tip
+        (Bin _ lk lx Tip (Bin _ lrk lrx _ _)) => Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)
+        (Bin _ lk lx ll@(Bin _ _ _ _ _) Tip) => Bin 3 lk lx ll (Bin 1 k x Tip Tip)
+        (Bin ls lk lx ll@(Bin lls _ _ _ _) lr@(Bin lrs lrk lrx lrl lrr)) =>
+          if lrs < ratio*lls
+            then Bin (1+ls) lk lx ll (Bin (1+lrs) k x lr Tip)
+            else Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+size lrr) k x lrr Tip)
+
+    (Bin rs _ _ _ _) =>
+      case l of
+        Tip => Bin (1+rs) k x Tip r
+        (Bin ls lk lx ll lr) =>
+          if ls > delta*rs
+            then case (ll, lr) of
+              (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) =>
+                if lrs < ratio*lls
+                  then Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r)
+                  else Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r)
+              (_, _) => raise "Failure in Data.Map.balanceL"
+            else Bin (1+ls+rs) k x l r
+
+-- balanceR is called when right subtree might have been inserted to or when
+-- left subtree might have been deleted from.
+balanceR : k -> a -> Map k a -> Map k a -> Map k a
+balanceR k x l r =
+  case l of
+    Tip =>
+      case r of
+        Tip => Bin 1 k x Tip Tip
+        (Bin _ _ _ Tip Tip) => Bin 2 k x Tip r
+        (Bin _ rk rx Tip rr@(Bin _ _ _ _ _)) => Bin 3 rk rx (Bin 1 k x Tip Tip) rr
+        (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) => Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)
+        (Bin rs rk rx rl@(Bin rls rlk rlx rll rlr) rr@(Bin rrs _ _ _ _)) =>
+          if rls < ratio*rrs
+            then Bin (1+rs) rk rx (Bin (1+rls) k x Tip rl) rr
+            else Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
+    (Bin ls _ _ _ _) =>
+      case r of
+        Tip => Bin (1+ls) k x l Tip
+        (Bin rs rk rx rl rr) =>
+          if rs > delta*ls
+            then case (rl, rr) of
+              (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) =>
+                if  rls < ratio*rrs
+                  then Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr
+                  else Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr)
+              (_, _) => raise "Failure in Data.Map.balanceR"
+            else Bin (1+ls+rs) k x l r
+
+
+-- | /O(log n)/. Insert a new key and value in the map.
+-- If the key is already present in the map, the associated value is
+-- replaced with the supplied value. 'insert' is equivalent to
+-- @'insertWith' 'const'@.
+--
+-- > insert 5 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'x')]
+-- > insert 7 'x' (fromList [(5,'a'), (3,'b')]) == fromList [(3, 'b'), (5, 'a'), (7, 'x')]
+-- > insert 5 'x' empty                         == singleton 5 'x'
+--
+-- See Map.Internal.Note: Type of local 'go' function
+public export
+insert : Ord k => k -> a -> Map k a -> Map k a
+insert = go where
+  go : Ord k => k -> a -> Map k a -> Map k a
+  go kx x Tip = singleton kx x
+  go kx x (Bin sz ky y l r) =
+    case compare kx ky of
+      LT => balanceL ky y (go kx x l) r
+      GT => balanceR ky y l (go kx x r)
+      EQ => Bin sz kx x l r
+
+-- | /O(log n)/. Lookup the value at a key in the map.
+--
+-- The function will return the corresponding value as @('Just' value)@,
+-- or 'Nothing' if the key isn't in the map.
+--
+-- An example of using @lookup@:
+--
+-- > import Prelude hiding (lookup)
+-- > import Data.Map
+-- >
+-- > employeeDept = fromList([("John","Sales"), ("Bob","IT")])
+-- > deptCountry = fromList([("IT","USA"), ("Sales","France")])
+-- > countryCurrency = fromList([("USA", "Dollar"), ("France", "Euro")])
+-- >
+-- > employeeCurrency : String -> Maybe String
+-- > employeeCurrency name = do
+-- >     dept <- lookup name employeeDept
+-- >     country <- lookup dept deptCountry
+-- >     lookup country countryCurrency
+-- >
+-- > main = do
+-- >     putStrLn \$ "John's currency: " ++ (show (employeeCurrency "John"))
+-- >     putStrLn \$ "Pete's currency: " ++ (show (employeeCurrency "Pete"))
+--
+-- The output of this program:
+--
+-- >   John's currency: Just "Euro"
+-- >   Pete's currency: Nothing
+public export
+lookup : Ord k => k -> Map k a -> Maybe a
+lookup = go where
+  go _ Tip = Nothing
+  go k (Bin _ kx x l r) =
+    case compare k kx of
+      LT => go k l
+      GT => go k r
+      EQ => Just x
+
diff --git a/Idris/Main.idr b/Idris/Main.idr
@@ -0,0 +1,74 @@
+-- The following program is a simple test for the following conjecture:
+
+-- Let S: N -> N be the sum of the digits of a positive integer.
+-- For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.
+
+module Main
+
+import System
+import Data.Map
+
+main : IO Int
+main = do
+    args <- getArgs
+
+    case head' args >>= Just . readDec of
+      Just [(max, "")] =>
+        if counter' max then exitFailure else exitSuccess
+      _ => exitInvalidInput
+
+    where
+      head' : List a -> Maybe a
+      head' [] = Nothing
+      head' xs = Just (head xs)
+
+-- Calculates the sum of the digits of `n`.
+sum' : Nat -> Int
+sum' n
+     | n < 10 = fromEnum n
+     | otherwise = fromEnum (n `mod` 10) + sum' (n `div` 10)
+
+-- Returns `Just updated` if the if the conjecture holds for pair, where
+-- `updated` is an updated versions of the sums cache provided by `sums`.
+-- Otherwise returns `Nothing`.
+test' : Map Nat Int -> (Nat, Nat) -> Maybe (Map Nat Int)
+test' sums pair =
+    case diff sums pair of
+        Left updated =>
+            test' updated pair
+
+        Right dif =>
+            if dif `mod` 9 == 0 then Just sums else Nothing
+
+-- Given a cache of the image of `sum'`, attemps to lookup `sum' a`, `sum' b`
+-- and `sum' \$ a + b`.
+-- If the lookup succeeds, returns `Right (sum' (a + b) - sum' a - sum' a)`.
+-- Otherwise inserts the value that caused the failure to `sums` and returns
+-- `Left sums`.
+diff : Map Nat Int -> (Nat, Nat) -> Either (Map Nat Int) Int
+diff sums (a, b) = do
+    sa  <- lookupOrInsert a
+    sb  <- lookupOrInsert b
+    sab <- lookupOrInsert \$ a + b
+
+    return \$ sab - sa - sb
+    where lookupOrInsert x =
+            case Data.Map.lookup x sums of
+                Just sx => Right sx
+
+                Nothing => Left (insert x (sum' x) sums)
+
+-- Checks if there is any counterexample in
+-- [(a, b) | a <- [0..max], b <- [a..max]].
+--
+-- Returns `True` if a counter example was found.
+-- Otherwise returns `False`.
+counter' : Nat -> Bool
+counter' max =
+    case foldM test' empty [(a, b) | a <- [0..max], b <- [a..max]] of
+        Nothing => True
+        Just _  => False
+
+exitInvalidInput : IO Int
+exitInvalidInput = exitWith \$ ExitFailure 2
+
diff --git a/README.md b/README.md
@@ -29,16 +29,19 @@ The conjecture was [proved by exhaustion](https://en.wikipedia.org/wiki/Proof_by
_* out of date_

# Contributing
-Contributions are welcomed! If you want to create a solution in a different language or improve the work on an existing implementation, feel free to help out.
+
+Contributions are welcomed! If you want to create a solution in a different
+language or improve the work on an existing implementation, feel free to help
+out.

However, there are some guidelines.

## The Algorithm

-The program should test the conjecture **for all pairs `(a, b)` where `0 <= a <= MAX`**
-**and `0 <= b <= a`**, as this is sufficient to proof the conjecture
-**for all pairs `(a, b)` between `0` and `MAX`**. The value of `MAX` should be provided in
-the first command-line argument.
+The program should test the conjecture **for all pairs `(a, b)` where
+`0 <= a <= MAX` and `0 <= b <= a`**, as this is sufficient to proof the
+conjecture **for all pairs `(a, b)` between `0` and `MAX`**. The value of `MAX`
+should be provided in the first command-line argument.

The following algorithm should be used:

@@ -55,12 +58,13 @@ Alternativelly, one could iterate `b` between `a` and `MAX`.

### Concurency

-The use of concurrency is encoraged for implementations on languages that provide good
-support for it. In the case concurrency is used, an additional, optional parameter `NPROCESSES`
-should be passed to the application in the seccond command-line argument.
+The use of concurrency is encoraged for implementations on languages that
+provide good support for it. In the case concurrency is used, an additional,
+optional parameter `NPROCESSES` should be passed to the application in the
+seccond command-line argument.

-The default value of `NPROCESSES` should be `1`. The algorithm should then be addapted to the
-following:
+The default value of `NPROCESSES` should be `1`. The algorithm should then be
+addapted to the following:

```
for i between 0 and NPROCESSES:
@@ -84,5 +88,7 @@ for a between 0 and MAX by steps of NPROCESSES:
signal to the main process that no counterexample was found
```

-The routine should only signal wheter or not a counterexample was found.
+This scheme ensures computations are envenlly distributed across processes.
+Note that the routine should only signal wheter or not a counterexample was
+found.

diff --git a/Wasm/main.wat b/Wasm/main.wat
@@ -1,32 +1,54 @@
+;; The following program is a simple test for the following conjecture:
+
+;; Let S: N -> N be the sum of the digits of a positive integer.
+;; For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.
+
(module
-    ;; Check if the is any counterexample in {(x, y) | 0 <= x <= a, 0 <= y <= x}
+    ;; Check if there is any counterexample
+    ;; in {(x, y) | 0 <= x <= a, 0 <= y <= x}
(func (export "counterexempl") (param \$a i32) (result i32)
(local \$b i32)

-        (block \$break_0     ;; while a != 0
-        (loop \$while_0
-                (br_if \$break_0 (i32.eqz (local.get \$a)))
-            (local.set \$b (local.get \$a))                           ;; b = a
+        ;; while a != 0
+        (block \$break_0
+               (loop \$while_0
+                     (br_if \$break_0 (i32.eqz (local.get \$a)))
+
+                     ;; b = a
+                     (local.set \$b (local.get \$a))

-                (block \$break_1                                         ;; while b != 0
-                (loop \$while_1
-                (br_if \$break_1 (i32.eqz (local.get \$b)))
-            (if (call \$test (local.get \$a) (local.get \$b))                  ;; if test(a, b)
-                            (block (i32.const 1) (return))                              ;; return 1
-                            (block                                                      ;; else
-                    (local.set \$b (i32.sub (local.get \$b) (i32.const 1)))   ;; b -= 1
-                    (br \$while_1)                                           ;; continue
+                     ;; while b != 0
+                     (block \$break_1
+                            (loop \$while_1
+                                  (br_if \$break_1 (i32.eqz (local.get \$b)))
+                                  (if ;; if test(a, b)
+                                    (call \$test (local.get \$a) (local.get \$b))
+
+                                    ;; return 1
+                                    (block (i32.const 1) (return))
+
+                                    (block ;; else
+
+                                      ;; b -= 1
+                                      (local.set \$b
+                                                 (i32.sub
+                                                   (local.get \$b)
+                                                   (i32.const 1)
+                                                 )
+                                      )
+                                      (br \$while_1) ;; continue
+                                    )
+                                  )
)
-            )
-                )
-                )
-
-            (local.set \$a (i32.sub (local.get \$a) (i32.const 1)))   ;; a -= 1
-            (br \$while_0)                                           ;; continue
-        )
+                     )
+
+                     ;; a -= 1
+                     (local.set \$a (i32.sub (local.get \$a) (i32.const 1)))
+                     (br \$while_0) ;; continue
+               )
)

-        (i32.const 0)   ;; return 0
+        (i32.const 0) ;; return 0
)

;; Calculates the sums of the digits of a non-negative integer.
@@ -35,41 +57,44 @@
(local.set \$sum (i32.const 0))

(block \$break
-        (loop \$while
-            ;; Break if n == 0i32
-            (br_if \$break (i32.eqz (local.get \$n)))
-
-            ;; sum += n % 10
-            (local.set \$sum
-            (i32.add
-                        (local.get \$sum)
-                (i32.rem_u (local.get \$n) (i32.const 10))
-            )
-            )
+               (loop \$while
+                     ;; Break if n == 0i32
+                     (br_if \$break (i32.eqz (local.get \$n)))
+
+                     ;; sum += n % 10
+                     (local.set \$sum
+                                (i32.add
+                                  (local.get \$sum)
+                                  (i32.rem_u (local.get \$n) (i32.const 10))
+                                )
+                     )
+
+                     ;; n /= 10
+                     (local.set \$n (i32.div_u (local.get \$n) (i32.const 10)))

-            ;; n /= 10
-            (local.set \$n (i32.div_u (local.get \$n) (i32.const 10)))
-
-            ;; Go to `while`
-            (br \$while)
-        )
+                     ;; Go to `while`
+                     (br \$while)
+               )
)

-        (local.get \$sum)    ;; return sum
+        (local.get \$sum) ;; return sum
)

;; Checks if (sum_digits(a + b) - (sum_digits(a) + sum_digits(b))) % 9 != 0
(func \$test (export "test") (param \$a i32) (param \$b i32) (result i32)
-        (i32.ne
+          (i32.ne
(i32.const 0)
-        (i32.rem_s
-        (i32.sub
-            (call \$sum_digits (i32.add (local.get \$a) (local.get \$b)))
-            (i32.add (call \$sum_digits (local.get \$a)) (call \$sum_digits (local.get \$b)))
-        )
-            (i32.const 9)
-        )
-    )
+            (i32.rem_s
+              (i32.sub
+                (call \$sum_digits (i32.add (local.get \$a) (local.get \$b)))
+                (i32.add
+                  (call \$sum_digits (local.get \$a))
+                  (call \$sum_digits (local.get \$b))
+                )
+              )
+              (i32.const 9)
+            )
+          )
)
)

```