五色定理 in Egison

5color.egi

--
-- 5-color
--
-- Egison Jornal Vol.2 「Egison パターンマッチによるグラフの彩色」を new syntax で書いたもの
--
-- $ egison                                       4.1.3
-- > loadFile "5color.egi"


--
-- Matcher
--
def mNode  := (integer, (maybe integer))
def mGraph := multiset (mNode, (list mNode))


--
-- Codes
--
def N := 5

-- main routine
def fiveColor gData :=
  match gData as mGraph with
    -- 次数が 5以下 で色が塗られていないノードを取り除く
  | ((($id, nothing), !(_ :: (loop $i (2, N + 1) (_ :: ...) _))) & $nodeInfo) :: _
      -> colorize id $ addNode nodeInfo $ fiveColor $ removeNode id gData
  | _ -> gData

def removeNode id :=
  \matchAll as mGraph with
  | (!((#id, _), _) & ($nid, $edges)) :: _
    -> (nid, (matchAll edges as (multiset mNode) with (!(#id, _) & $n) :: _ -> n))

def addNode nodeInfo gData :=
  [(fst nodeInfo, (matchAll (snd nodeInfo, gData) as (set mNode, mGraph) with
    | (($id, _)  :: _,   (#id, $c) :: _ ) -> (id, c)
    | (($id, $c) :: _, !((#id,  _) :: _)) -> (id, c)    
    ))]
  ++ matchAll (gData, snd nodeInfo) as (mGraph, set mNode) with
      | ((($id, $c), $edges) :: _,   (#id, _) :: _ ) -> ((id, c), [fst nodeInfo] ++ edges) 
      | ((($id, $c), $edges) :: _, !((#id, _) :: _)) -> ((id, c),                   edges) 

def colorize id gData :=
  match ([1..5], gData) as (set integer, mGraph) with
    -- 周りのノードでまだ 5色 全部使われていない場合
  | ($c :: _, (((#id, nothing), !(_ ++ (_, (just #c)) :: _)) :: _)) -> assignColor id c gData
    -- 次数が 5 で周りで 5色全部使われているノードしか残っていない場合
  | (_,       (((#id, nothing), ($nid_1, (just $c_1)) :: (loop $i (2, N) (($nid_i, (just $c_i)) :: ...) []) ) :: _)) 
    -> match gData as mGraph with
          -- 色1 と 色3 のみで ノード1 と ノード3 が繋がるパターン
        | ((#nid_1, _), _ ++ ($cnid_1, ((just #c_1) | (just #c_3))) :: _)
          :: (loop $i (2, N) (((#cnid_(i - 1), _), _ ++ ($cnid_i, ((just #c_1) | (just #c_3))) :: _) :: ...)
                             (((#cnid_n,       _), _ ++ (#nid_3,  ((just #c_1) | (just #c_3))) :: _)))
              -- 色2 と 色4 を順番に書き換える
            -> assignColor id c_2 $ flipColor3 id nid_2 c_2 c_4 gData $ twoColorSubgraph nid_2 c_2 c_4 gData
          -- ノード1 と ノード3 が繋がらないパターン
        | _ -> assignColor id c_1 $ flipColor3 id nid_1 c_1 c_3 gData $ twoColorSubgraph nid_1 c_1 c_3 gData

def flipColor id1 id2 c1 c2 gData :=
  match gData as mGraph with
  | ((#id2, (just #c1)), _ ++ (($id3, (just #c2)) & !(#id1, _)) :: _) :: _
      -> assignColor id2 c2 $ flipColor id2 id3 c2 c1 gData
  | _ -> assignColor id2 c2 gData

def assignColor id c :=
  map (\n -> (rewriteNode id c ((2)#%1 n), (map (\k -> rewriteNode id c k) ((2)#%2 n)))) where
    rewriteNode id c n := match n as mNode with
      | (#id, _) -> (id, (Just c))
      | _        -> n

-- ------------------------------------
def twoColorSubgraph sid c1 c2 gData :=
  unique $ matchAll gData as mGraph with
  | ((#sid, _), _ ++ ($id_1, ((just #c1) | (just #c2))) :: _)
    :: (loop $i
             (1, $n)
             (((#id_i,       ((just #c1) | (just #c2))), _ ++ ($id_(i + 1), ((just #c1) | (just #c2))) :: _) :: ...)
             (((#id_(n + 1), ((just #c1) | (just #c2))), _ ++ ($rid,        ((just #c1) | (just #c2)) & $rc) :: _) :: _))
      -> (rid, rc)

def flipColor2 c1 c2 gData :=
  \match as (list mNode) with
  | ($id, (just #c1)) :: $xs -> flipColor2 c1 c2 (assignColor id c2 gData) xs
  | ($id, (just #c2)) :: $xs -> flipColor2 c1 c2 (assignColor id c1 gData) xs
  | _ -> gData

def flipColor3 id nid c1 c3 gData sub :=
  if sub = [] then
    flipColor id nid c1 c3 gData
  else
    flipColor2       c1 c3 gData sub


--
-- Data
--
def graphData1 :=
  [((1, Nothing), [(2, Nothing)]),
   ((2, Nothing), [(1, Nothing)])]
def graphData2 :=
  [((1, Nothing), [(2, Nothing), (3, Nothing)]),
   ((2, Nothing), [(3, Nothing), (1, Nothing)]),
   ((3, Nothing), [(1, Nothing), (2, Nothing)])] -- K3
def graphData3 :=
  [((1, Nothing), [(2, (Just 1))]),
   ((2, (Just 1)), [(3, (Just 2)), (1, Nothing)]),
   ((3, (Just 2)), [(4, (Just 1)), (2, (Just 1))]),
   ((4, (Just 1)), [(5, (Just 2)), (3, (Just 2))]),
   ((5, (Just 2)), [(4, (Just 1))])]
def graphData4 :=
  [((1, Nothing), [(2, (Just 1))]),
   ((2, (Just 1)), [(3, (Just 2)), (1, Nothing)]),
   ((3, (Just 2)), [(4, (Just 1)), (2, (Just 1))]),
   ((4, (Just 1)), [(5, (Just 2)), (3, (Just 2)), (6, (Just 2))]),
   ((5, (Just 2)), [(4, (Just 1))]),
   ((6, (Just 2)), [(4, (Just 1))])]
def graphData5 :=
  [((0, Nothing), [(1, (Just 1)), (2, (Just 2)), (3, (Just 3)), (4, (Just 4)), (5, (Just 5))]),
   ((1, (Just 1)), [(2, (Just 2)), (0, Nothing), (5, (Just 5))]),
   ((2, (Just 2)), [(3, (Just 3)), (0, Nothing), (1, (Just 1))]),
   ((3, (Just 3)), [(4, (Just 4)), (0, Nothing), (2, (Just 2))]),
   ((4, (Just 4)), [(5, (Just 5)), (0, Nothing), (3, (Just 3))]),
   ((5, (Just 5)), [(1, (Just 1)), (0, Nothing), (4, (Just 4))])] -- C5


--
-- Tests
--
-- $ egison -t 5color.egi
assertEqual "test1"
  (addNode ((1,Nothing),[(2,Nothing)]) $ removeNode 1 graphData1)
  [((1, Nothing), [(2, Nothing)]), ((2, Nothing), [(1, Nothing)])]

assertEqual "test2"
  (assignColor 1 2 graphData2)
  [((1, Just 2), [(2, Nothing), (3, Nothing)]), ((2, Nothing), [(3, Nothing), (1, Just 2)]), ((3, Nothing), [(1, Just 2), (2, Nothing)])]

assertEqual "test3"
  (flipColor 1 2 1 2 graphData3)
  [((1, Nothing), [(2, Just 2)]), ((2, Just 2), [(3, Just 1), (1, Nothing)]), ((3, Just 1), [(4, Just 2), (2, Just 2)]), ((4, Just 2), [(5, Just 1), (3, Just 1)]), ((5, Just 1), [(4, Just 2)])]

assertEqual "test4ng"
  (flipColor 1 2 1 2 graphData4)
  [((1, Nothing), [(2, Just 2)]), ((2, Just 2), [(3, Just 1), (1, Nothing)]), ((3, Just 1), [(4, Just 2), (2, Just 2)]), ((4, Just 2), [(5, Just 1), (3, Just 1), (6, Just 2)]), ((5, Just 1), [(4, Just 2)]), ((6, Just 2), [(4, Just 2)])]

assertEqual "test5"
  (fiveColor graphData5)
  [((0, Just 1), [(1, Just 3), (2, Just 2), (3, Just 3), (4, Just 4), (5, Just 5)]), ((1, Just 3), [(0, Just 1), (2, Just 2), (5, Just 5)]), ((2, Just 2), [(0, Just 1), (3, Just 3), (1, Just 3)]), ((3, Just 3), [(0, Just 1), (4, Just 4), (2, Just 2)]), ((4, Just 4), [(0, Just 1), (5, Just 5), (3, Just 3)]), ((5, Just 5), [(0, Just 1), (1, Just 3), (4, Just 4)])]

assertEqual "test6"
  (twoColorSubgraph 1 1 2 graphData4)
  [(3, Just 2), (4, Just 1), (2, Just 1), (5, Just 2), (6, Just 2)]

assertEqual "test7ok"
  (flipColor2 1 2 graphData4 (twoColorSubgraph 1 1 2 graphData4))
  [((1, Nothing), [(2, Just 2)]), ((2, Just 2), [(3, Just 1), (1, Nothing)]), ((3, Just 1), [(4, Just 2), (2, Just 2)]), ((4, Just 2), [(5, Just 1), (3, Just 1), (6, Just 1)]), ((5, Just 1), [(4, Just 2)]), ((6, Just 1), [(4, Just 2)])]