計算モデルの数理の変更点

追加された行はこの色です。
削除された行はこの色です。
計算モデルの数理へ行く。
計算モデルの数理の差分を削除
[[講義日程-2008年度夏学期]]

** 計算モデルの数理 [#lec6e708]
- 担当：武市 正人 教授, 胡 振江 准教授 
- 1.5単位
-- 数理：限定選択B
-- システム：限定選択C
-- 物工：限定選択※
- 8:30-10:00 工学部六号館 61講義室
- 講義ページ
-- [[胡先生>http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/teach/cm08/]]
-- [[武市先生>http://www.ipl.t.u-tokyo.ac.jp/~takeichi/pages/_34.html]]

-- [[去年のもの>http://www.ipl.t.u-tokyo.ac.jp/lecture/computation-model2007/]]
-昨年度は試験で教科書及びノートの持ち込み可だった模様。

**内容 [#da2b2f53]

-while文出しちゃうぞー(胡先生)
--末尾再帰ですか！わかりません！

-tzikのノートは今学期は[[blog>http://tzik.homeunix.net/tzik/blog/cat1/cat3/]]に書きます。

-ラムダ計算の基礎
--http://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-software-kougaku-2005/lambda.pdf
--http://d.hatena.ne.jp/m-hiyama/20070220/1171956186

-関係ないのだけど、入力メソッドのSKKのネーミングはこれから来ているらしい~
http://openlab.jp/skk/SKK.html

-Haskellでβ-簡約を実装した（最左戦略）。これで快適なλ生活があなたのものに！（ただし、チャーチ数の定義が普通のものとちょっとだけ違います。）
 module Lambda where
 import Data.List
 type Val = String
 data Lambda = V Val | A Lambda Lambda | L Val Lambda
 instance Show Lambda where
     show (V x) = x
     show (A m n) = show' m ++ show'' n 
         where 
           show' (V x) = x
           show' m@(A _ _) = show m
           show' m@(L _ _) = "("++ show m ++")"
           show'' (V x) = x
           show'' m@(A _ _) = "("++ show m ++")"
           show'' m@(L _ _) = "("++ show m ++")"
     show (L x m) = "\\"++ x ++ "."++ show m
 
 -- 変数
 vals ::[Val]
 vals = words "a b c d e f g h i j k l m n o p q r s u v w x y z"
 
 -- 代入
 subst :: Lambda -> Val -> Lambda -> Lambda 
 subst (V y) x n = if y==x then n else (V y)
 subst (A m1 m2) x n = subst m1 x n `A` subst m2 x n
 subst (L y m) x n = if y/=x && notElem y fn
                     then L y $ subst m x n 
                     else if null . (\\) vals $ fn++[y]++freeV m
                          then (V "too many variables")
                          else subst (L z $ subst m y $ V z ) x n 
                              where fn = freeV n
                                    z = last . (\\) vals $ fn++[y]++freeV m
 -- 自由変数
 freeV :: Lambda -> [Val]
 freeV (V x) = [x]
 freeV (A m n) = freeV m `union` freeV n
 freeV (L x m) = freeV m \\ [x]
 
 -- β-簡約
 beta :: Lambda -> Lambda 
 beta (V x) = V x
 beta (L x m) = L x $ beta m
 beta ((L x m) `A` n) = beta $ subst m x n
 beta ((V x) `A` m) = V x `A` beta m
 beta (m `A` n) = beta $ value m `A` n
 
 -- Value = V Val `A` Lambda | L Val `A` Lambda
 value :: Lambda -> Lambda
 value (V x) = V x
 value (L x m) = L x m
 value ((L x m) `A` n) = value $ subst m x n
 value ((V x) `A` m) =V x `A` value m
 value (m `A` n) = value $ value m `A` n
 
 -- one time (?) paralle beta-reduction
 pbeta :: Lambda -> Lambda 
 pbeta (V x) = V x
 pbeta (L x m) = L x $ pbeta m
 pbeta ((L x m) `A` n) = subst m x n
 pbeta (m `A` n) = pbeta m `A` pbeta n
 
 -- n times(?) paralle beta-reduction
 pbeta' n = foldl1 (.) . (take n ) . repeat $ pbeta
 
 -- よく使う変数
 u = V "u"
 v = V "v"
 w = V "w"
 x = V "x"
 y = V "y"
 z = V "z"
 
 -- Combinator
 i = L "x" x
 k = L "x" $ L "y"  x
 s = L "x" $ L "y" $ L "z" $ x`A`z`A`(y`A`z)
 b = L "x" $ L "y" $ L "z" $ x`A`(y`A`z)
 c = L "x" $ L "y" $ L "z" $ x`A`z`A`y
 q = L "y" $ lam `A` lam
     where lam = L "x" $ y `A` ( x`A`x)
 m = L "x" $ x `A` x
 o  =m `A` m
 
 -- 不動点演算子 theta
 theta = th `A` th 
 th = L "x" $ L "y" $ y `A` ( x `A` x `A` y)
 
 -- Church numeral 
 zero = L "z" $ L "y" z
 --zero = L"z" $ L "y" y
 one = beta $ suc `A` zero
 two = beta $ suc `A` one
 three = beta $ suc `A` two
 four = beta $ suc `A` three
 five = beta $ suc `A` four
 six = beta $ suc `A` five
 seven = beta $ suc `A` six
 eight = beta $ suc `A` seven
 nine = beta $ suc `A` eight
 
 -- 算術演算子
 suc = L "x" $ L "y" $ L "z" $ z `A` (x`A`y`A`z)
 --suc = L "x" $ L"y" $ L "z" $ y `A` (x `A` y `A` z)
 add  =L "x" $ L "y" $ y `A` x `A` suc
 mult =L "x" $ L "y" $ y `A` zero `A` (add `A` x)
 pre = L "x" $ L "y" $ L "z"$ x `A`(L"u" y)`A`t`A`(L"u" $ u)
     where t = L "g" $ L "h" $ V"h" `A` (V"g" `A` z)
 sub = L "x" $ L "y" $ y `A` x `A` pre 
 
 -- bool
 true = L "x" $ L "y" x
 false = L "x" $ L "y" y
 if' = L "x" $ L "y" $ L "z" $ x`A`y`A`z
 isZero = L "x" $ x `A` true `A` (L "y" false)
 leq = L "x" $ L "y" $ isZero `A` (sub `A` x `A` y)
 and' = L "x" $ L "y" $ if' `A` x `A` y `A` false
 or' =  L "x" $ L "y" $ if' `A` x `A` true `A` y
 neg = L"x" $ if' `A` x `A` false `A` true
 eq = L "x" $ L "y" $ and' `A` (leq `A` x `A` y) `A` (leq `A` y `A` x)
 even' = rec `A` neg `A` true 
 
 -- tuple 
 pair = L "x" $ L "y" $ L"z" $ z `A` x `A` y
 first = L "x" $ x `A` true
 second = L "x" $ x `A` false
 
 -- recursion
 -- f(0) = a
 -- f(n+1) = g(f(n))
 rec = L"g" $ L "a" $ L "x" $ x `A` V "a" `A` V "g"
 
 -- recursion2
 -- f(0) = a
 -- f(n+1) = g(f(n),n)
 rec2 = L "g" $ L "a" $ L "x" $ first `A` (rec `A` g' `A` a' `A` x)
     where g' = L "x" $ pair `A` (V "g" `A` (first `A` x) `A` (second `A` x)) `A` (suc `A` (second `A` x))
           a' = pair `A` V "a" `A` zero 
 
 -- halfCeil n は n/2以上の最小整数を返す
 halfCeil = rec2 `A` g `A` zero
     where g = L "x" $ L"y" $ if' `A` (even' `A` y) `A` (suc `A` x) `A` x
 
 
 -- 割ったあまり
 rem' = q `A` (L "z" $ L "x" $ L "y" g)
     where g = if' `A` (leq `A` y `A` x) `A` (z `A` (sub `A` x `A` y) `A`y) `A` x
 
 -- 階乗
 fact = L "x" $ (q `A` f) `A` x
     where f = L "fct" $ L "x" $ if' `A` (isZero `A` x) `A` one `A` (mult `A` x `A` (V "fct" `A` (pre `A` x)))
 
 -- 素数判定
 isPrime = L "x" $ if' `A` (eq `A` x `A` two) `A` true `A` f
     where f = if' `A` (eq `A` x `A` four) `A` false `A` ((q `A` g) `A` two)
           g = L "z" $ L "y" $ if' `A` (eq `A` y `A` (halfCeil `A` x)) `A` true `A` h
           h = if' `A` (isZero `A` (rem' `A` x`A` y)) `A` false `A` (z`A` (suc `A` y))
 
 -- Ackermann
 -- http://en.wikipedia.org/wiki/Ackermann_function
 ack = L "m" $ rec `A` iter `A` suc `A` V "m"
     where iter = L "f" $ rec `A` V "f" `A` (V "f" `A` one)
 -- Church numberからIntへの変換
 churchToInt :: Lambda -> Int
 churchToInt (L f (L x m)) = g m
     where g (V x) = 0
           g (V f `A` n) = 1 + (g n)
 -- IntからChurch numberへの変換
 intToChurch :: Int -> Lambda
 intToChurch 0 = zero
 intToChurch (n+1) =beta $  suc `A` (intToChurch n)
 
 -- ラムダ項からBoolへの変換
 lambdaToBool :: Lambda -> Bool
 lambdaToBool (L t (L f (V b))) = if t == b then True else False
計算モデルの数理 の変更点

計算モデルの数理の変更点
