Haskell - 数値 - 帰納法(完全帰納法、プログラム合成)

関数プログラミング入門
原著

開発環境

• macOS Sierra - Apple (OS)
• Emacs (Text Editor)
• Haskell (プログラミング言語)
• Haskell Platform(ghci)(処理系)

関数プログラミング入門(Richard Bird (著)、山下伸夫 (翻訳)、オーム社)の第3章(数値)、3.2(帰納法)、練習問題3.2.1、3.2.2、3.2.3、3.2.4、3.2.5、3.2.6、3.2.7を取り組んでみる。

練習問題3.2.1、3.2.2、3.2.3、3.2.4、3.2.5、3.2.6、3.2.7

コード(Emacs)

-- 3.2.1
-- (Succ Zero) * Zero = Zero
-- (Succ Zero) * (Succ n)
-- = ((Succ Zero) * n) + (Succ Zero)
-- = n + (Succ Zero)
-- = Succ (n + Zero)
-- = Succ n


-- 3.2.2
-- a +' x = a
-- a +' b = a
-- x +' b = b
-- a +' b = b
-- a = a +' b = b
-- a = b


-- 3.2.3
-- x ^ (m + undefined)
-- = x ^ undefined
-- = undefined

-- (x ^ m) * (x ^ undefined)
-- = (x * m) * undefined
-- = undefined

-- x ^ (m + undefined) = (x ^ m) * (x ^ undefined)


-- 3.2.4
-- (m + n) + undfined = undefined
-- m + (n + undefined) = m + undefined = undefined
-- (m + n) + undfined = m + (n + undefined)

-- (m + n) + Zero = m + n
-- m + (n + Zero) = m + n
-- (m + n) + Zero = m + (n + Zero)

-- (m + n) + (Succ p)
-- = Succ ((m + n) + p)
-- = Succ (m + (n + p))
-- = m + (Succ (n + p))
-- m + (n + (Succ p))
-- = m + (Succ (n + p))
-- = Succ (m + (n + p))
-- = m + (Succ (n + p))
-- (m + n) + (Succ p) = m + (n + (Succ p))


-- 3.2.5
-- undefined * (m + n) = undefined
-- (undefined * m) + (undefined * n)
-- = undefined + undefined
-- = undefined
-- undefined * (m + n) = (undefined * m) + (undefined * n)

-- Zero * (m + n) = Zero
-- (Zero * m) + (Zero * n)
-- = Zero + Zero
-- = Zero
-- Zero * (m + n) = Zero = (Zero * m) + (Zero * n)

-- (Succ k) * (m + n)
-- = (k * (m + n)) + (m + n)
-- = k * m + k * n + m + n
-- = k * m + m + k * n + n
-- = (Succ k) * m + (Succ k) * n


-- 3.2.6
op :: Nat -> Nat -> Nat
op m n = if m < n
         then m
         else n

-- undefined `op` Infinity =  undefined

-- Zero `op` Infinity = Zero
-- (Succ m) `op` Infinity
-- = (Succ m) `op` (Succ Infinity)
-- = Succ (m `op` Infinity)
-- = Succ Infinity
-- = Infinity

-- Infinity `op` Infinity = Infinity

data Nat = Zero | Succ Nat
  deriving (Eq, Ord, Show)

infinity :: Nat
infinity = Succ infinity

main :: IO ()
main = do
  print (Zero `op` infinity)
  print (Succ Zero `op` infinity)
  print (Succ (Succ (Succ (Succ (Succ Zero)))) `op` infinity)
  

入出力結果(Terminal, ghci)

$ runghc sample2.hs
Zero
Succ Zero
Succ (Succ (Succ (Succ (Succ Zero))))
$