仁木/メモ
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
単語検索
|
最終更新
|
ヘルプ
|
ログイン
]
開始行:
[[仁木]]
--------------------------
Reasoning about Haskell
定義
double :: Int->int
double x = x + x
------------------------
Simple examples
定義
reverse ::[a]->[a]
reverse [] =[]
reverse(x:xs) = reverse xs++[x]
----------------------------------
例
reverse[x]
=(list notation)
reverse(x:[])
=(applying reverse)
reverse[]++[x]
=(applying reverse)
[]++[x]
=(applying++)
[x]
---------------------------------------
Induction on numbers
定義
data Nat =Zero|Succ Nat
動作の例
Zero
Succ Zero
Succ(Succ Zero)
Succ(Succ(Succ Zero))
.
.
.
------------------------------------------
定義
add ::Nat->Nat->Nat
add Zero m = m
add (Succ n)m = Succ(add n m)
--------------------------------------------
例
1.
add Zero Zero
= (applying add)
Zero
2.
add(Succ n) Zero
=(applying add)
Succ(add n Zero)
=(insuction hypothesis)
Succ n
---------------------------------------------
Induction on lists
reverse(reverse[])
=(applying the innner reverse)
reverse[]
=(applying reverse)
[]
reverse(reverse(x:xs))
=(applying the inner reverse)
reverse(reverse xs++[x])
=(distributivity-see below)
reverse[x]++reverse(reverse xs)
=(single lists -see below)
[x]++xs
=(applying++)
x:xs
--------------------------------------
Making append vanish
reverse ::[a]->[a]
reverse xs = reverse'xs[]
reverse' ::[a]->[a]->[a]
reverse'[]ys =ys
reverse'(x:xs)ys = reverse' xs(x:ys)
--------------------------------------
例
reverse[1,2,3]
=(applying reverse)
reverse'[1,2,3][]
=(applying reverse')
reverse'[2,3](1:[])
=(applying reverse')
reverse'[3](2:(1:[]))
=(applying reverse')
reverse'[](3:(2:(1:[])))
=(applying reverse')
3:(2:(1:[]))
------------------------------------------
定義
data Expr = Val Int |Add Expr Expr
eval :: Expr->Int
eval(Val n) = n
eval(Add x y) = eval x + eval y
type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
exec ::Code ->Stack->Stack
exec [] s = s
exec(PUSH n:c)s = exec c(n:s)
exec(ADD:c)(m:n:s) = exec c(n+m:s)
comp ::Expr -> Code
comp(Val n) = [PUSH n]
comp(Add x y) = comp x ++comp y ++ [ADD]
---------------------------------------
e =(2+3)+4
>eval e
9
>comp e
[PUSH2,PUSH3,ADD,PUSH4,ADD]
>exec(comp e)[]
[9]
終了行:
[[仁木]]
--------------------------
Reasoning about Haskell
定義
double :: Int->int
double x = x + x
------------------------
Simple examples
定義
reverse ::[a]->[a]
reverse [] =[]
reverse(x:xs) = reverse xs++[x]
----------------------------------
例
reverse[x]
=(list notation)
reverse(x:[])
=(applying reverse)
reverse[]++[x]
=(applying reverse)
[]++[x]
=(applying++)
[x]
---------------------------------------
Induction on numbers
定義
data Nat =Zero|Succ Nat
動作の例
Zero
Succ Zero
Succ(Succ Zero)
Succ(Succ(Succ Zero))
.
.
.
------------------------------------------
定義
add ::Nat->Nat->Nat
add Zero m = m
add (Succ n)m = Succ(add n m)
--------------------------------------------
例
1.
add Zero Zero
= (applying add)
Zero
2.
add(Succ n) Zero
=(applying add)
Succ(add n Zero)
=(insuction hypothesis)
Succ n
---------------------------------------------
Induction on lists
reverse(reverse[])
=(applying the innner reverse)
reverse[]
=(applying reverse)
[]
reverse(reverse(x:xs))
=(applying the inner reverse)
reverse(reverse xs++[x])
=(distributivity-see below)
reverse[x]++reverse(reverse xs)
=(single lists -see below)
[x]++xs
=(applying++)
x:xs
--------------------------------------
Making append vanish
reverse ::[a]->[a]
reverse xs = reverse'xs[]
reverse' ::[a]->[a]->[a]
reverse'[]ys =ys
reverse'(x:xs)ys = reverse' xs(x:ys)
--------------------------------------
例
reverse[1,2,3]
=(applying reverse)
reverse'[1,2,3][]
=(applying reverse')
reverse'[2,3](1:[])
=(applying reverse')
reverse'[3](2:(1:[]))
=(applying reverse')
reverse'[](3:(2:(1:[])))
=(applying reverse')
3:(2:(1:[]))
------------------------------------------
定義
data Expr = Val Int |Add Expr Expr
eval :: Expr->Int
eval(Val n) = n
eval(Add x y) = eval x + eval y
type Stack = [Int]
type Code = [Op]
data Op = PUSH Int | ADD
exec ::Code ->Stack->Stack
exec [] s = s
exec(PUSH n:c)s = exec c(n:s)
exec(ADD:c)(m:n:s) = exec c(n+m:s)
comp ::Expr -> Code
comp(Val n) = [PUSH n]
comp(Add x y) = comp x ++comp y ++ [ADD]
---------------------------------------
e =(2+3)+4
>eval e
9
>comp e
[PUSH2,PUSH3,ADD,PUSH4,ADD]
>exec(comp e)[]
[9]
ページ名: