計算モデルの数理
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
単語検索
|
最終更新
|
ヘルプ
] [
リンク元
]
開始行:
[[講義日程-2008年度夏学期]]
** 計算モデルの数理 [#lec6e708]
- 担当：武市 正人 教授, 胡 振江 准教授
- 1.5単位
-- 数理：限定選択B
-- システム：限定選択C
-- 物工：限定選択※
- 8:30-10:00 工学部六号館 61講義室
- 講義ページ
-- [[胡先生>http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/teach/...
-- [[武市先生>http://www.ipl.t.u-tokyo.ac.jp/~takeichi/pa...
-- [[去年のもの>http://www.ipl.t.u-tokyo.ac.jp/lecture/co...
-昨年度は試験で教科書及びノートの持ち込み可だった模様。
**内容 [#da2b2f53]
-while文出しちゃうぞー(胡先生)
--末尾再帰ですか！わかりません！
-tzikのノートは今学期は[[blog>http://tzik.homeunix.net/tz...
-ラムダ計算の基礎
--http://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-s...
--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 ...
-- 代入
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]++...
then (V "too many variables")
else subst (L z $ subst m y $ V...
where fn = freeV n
z = last . (\\) vals ...
-- 自由変数
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" $...
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...
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`...
where g' = L "x" $ pair `A` (V "g" `A` (first `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` (...
-- 割ったあまり
rem' = q `A` (L "z" $ L "x" $ L "y" g)
where g = if' `A` (leq `A` y `A` x) `A` (z `A` (sub ...
-- 階乗
fact = L "x" $ (q `A` f) `A` x
where f = L "fct" $ L "x" $ if' `A` (isZero `A` x) `...
-- 素数判定
isPrime = L "x" $ if' `A` (eq `A` x `A` two) `A` true `A...
where f = if' `A` (eq `A` x `A` four) `A` false `A` ...
g = L "z" $ L "y" $ if' `A` (eq `A` y `A` (hal...
h = if' `A` (isZero `A` (rem' `A` x`A` y)) `A`...
-- 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 els...
終了行:
[[講義日程-2008年度夏学期]]
** 計算モデルの数理 [#lec6e708]
- 担当：武市 正人 教授, 胡 振江 准教授
- 1.5単位
-- 数理：限定選択B
-- システム：限定選択C
-- 物工：限定選択※
- 8:30-10:00 工学部六号館 61講義室
- 講義ページ
-- [[胡先生>http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/teach/...
-- [[武市先生>http://www.ipl.t.u-tokyo.ac.jp/~takeichi/pa...
-- [[去年のもの>http://www.ipl.t.u-tokyo.ac.jp/lecture/co...
-昨年度は試験で教科書及びノートの持ち込み可だった模様。
**内容 [#da2b2f53]
-while文出しちゃうぞー(胡先生)
--末尾再帰ですか！わかりません！
-tzikのノートは今学期は[[blog>http://tzik.homeunix.net/tz...
-ラムダ計算の基礎
--http://www.kb.ecei.tohoku.ac.jp/~sumii/class/keisanki-s...
--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 ...
-- 代入
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]++...
then (V "too many variables")
else subst (L z $ subst m y $ V...
where fn = freeV n
z = last . (\\) vals ...
-- 自由変数
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" $...
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...
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`...
where g' = L "x" $ pair `A` (V "g" `A` (first `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` (...
-- 割ったあまり
rem' = q `A` (L "z" $ L "x" $ L "y" g)
where g = if' `A` (leq `A` y `A` x) `A` (z `A` (sub ...
-- 階乗
fact = L "x" $ (q `A` f) `A` x
where f = L "fct" $ L "x" $ if' `A` (isZero `A` x) `...
-- 素数判定
isPrime = L "x" $ if' `A` (eq `A` x `A` two) `A` true `A...
where f = if' `A` (eq `A` x `A` four) `A` false `A` ...
g = L "z" $ L "y" $ if' `A` (eq `A` y `A` (hal...
h = if' `A` (isZero `A` (rem' `A` x`A` y)) `A`...
-- 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 els...
ページ名:
![[PukiWiki]](image/pukiwiki.png "[PukiWiki]")
