「計算と論理」 Software Foundations その3
|
|
|
- くにひと いちぞの
- 5 years ago
- Views:
Transcription
1 Software Foundations 3 cal17@fos.kuis.kyoto-u.ac.jp October 24, 2017 ( ) ( 3) October 24, / 47
2 Lists.v ( ) ( ) ( ) ( 3) October 24, / 47
3 ( ) Inductive natprod : Type := pair : nat nat natprod. pair: natprod pair 1 2 : natprod pair (4 + 3) 2 : natprod natprod ( ) pair product ( ) ( ) ( 3) October 24, / 47
4 : Definition fst (p : natprod) : nat := match p with pair x y => x (*! *) end. Definition snd (p : natprod) : nat := match p with pair x y => y end. fst (first projection) snd (second projection) ( ) ( 3) October 24, / 47
5 Notation Notation "( x, y )" := (pair x y). Definition fst (p : natprod) : nat := match p with (x,y) => x (*! *) end. Definition swap_pair (p : natprod) : natprod := match p with (x,y) => (y,x) end. ( ) ( 3) October 24, / 47
6 : Surjectivity of pairing ( ) Coq 1 Theorem surjective_pairing : forall (n m : nat), (n,m) = (fst (n,m), snd (n,m)). Proof. reflexivity. Qed. ( ) ( 3) October 24, / 47
7 2 Theorem surjective_pairing : forall (p : natprod), p = (fst p, snd p). Proof. intros p. destruct p as [n m]. reflexivity. Qed. natprod (n,m) induction ( ) ( 3) October 24, / 47
8 Lists.v ( ) ( ) ( ) ( 3) October 24, / 47
9 ( ) : (nil) ( ) (cons) ( ) ( 3) October 24, / 47
10 Inductive natlist : Type := nil : natlist cons : nat -> natlist -> natlist. ( ) : (nil) n l (cons n l)! ( ) ( 3) October 24, / 47
11 cons n :: l [n; m;...].v : Definition mylist1 := 1 :: (2 :: (3 :: nil)). Definition mylist2 := 1 :: 2 :: 3 :: nil. Definition mylist3 := [1;2;3]. ( ) ( 3) October 24, / 47
12 (1): repeat n count Fixpoint repeat (n count : nat) : natlist := match count with O => nil S count => n :: (repeat n count ) end. : let rec repeat n count = if count = 0 then [] else n :: repeat n (count - 1) ( ) ( 3) October 24, / 47
13 (2): length : Fixpoint length (l:natlist) : nat := match l with nil => O h :: t => S (length t) end. : let rec length l = match l with [] -> 0 _ :: t => length t + 1 ( ) ( 3) October 24, / 47
14 Example nil h :: t = h :: t t ( ) ( ) ( 3) October 24, / 47
15 (3): app(end) Fixpoint app (l1 l2 : natlist) : natlist := match l1 with nil => l2 h :: t => h :: (app t l2) end. : let rec append l1 l2 = match l1 with [] -> l2 h :: t -> h :: (append t l2) ( ) ( 3) October 24, / 47
16 app l1 l2 ( ) : l1 ++ l2 Example test_app1: [1;2;3] ++ [4] = [1;2;3;4]. Example test_app2: nil ++ [4;5] = [4;5]. Example test_app3: [1;2;3] ++ nil = [1;2;3]. ( ) ( 3) October 24, / 47
17 (4): hd, tl Definition hd (default:nat) (l:natlist) : nat := match l with nil => default h :: t => h end. Definition tl (l:natlist) : natlist := match l with nil => nil h :: t => t end. nil (default) ( ) ( 3) October 24, / 47
18 Lists.v ( ) ( ) ( ) ( 3) October 24, / 47
19 vs Inductive natlist : Type := nil : natlist cons : nat -> natlist -> natlist. Inductive nat : Type := O : nat S : nat -> nat.! ( ) ( 3) October 24, / 47
20 vs (2) Fixpoint app (l1 l2 : natlist) : natlist := match l1 with nil => l2 cons h t => cons h (app t l2) end. Fixpoint plus (n m : nat) : nat := match n with O => m S n => S (plus n m) end. ( ) ( 3) October 24, / 47
21 Theorem nil_app : forall l:natlist, [] ++ l = l. Proof. intros l. reflexivity. Qed. Theorem app_nil_end : forall l:natlist, l ++ [] = l. ( ) ( 3) October 24, / 47
22 Theorem tl_length_pred : forall l:natlist, pred (length l) = length (tl l). Proof. intros l. destruct l as [ n l ]. - (* l = nil *) reflexivity. - (* l = cons n l *) reflexivity. Qed. l = n :: l ( ) ( 3) October 24, / 47
23 P(l) ( ) l l P(l) P(nil) n l P(l ) P(n::l ) P(n::l ) P ( P(l )) P(l ) (induction hypothesis, IH) ( ) ( 3) October 24, / 47
24 : P(n) n P(n) P(0) n P(n ) P(S n ) P(S n ) P ( P(n )) P(n ) (induction hypothesis, IH) ( ) ( 3) October 24, / 47
25 ++ Theorem app_assoc : forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3). Proof. intros l1 l2 l3. induction l1 as [ n l1 ]. - (* l1 = nil *) reflexivity. - (* l1 = cons n l1 *) simpl. rewrite -> IHl1. reflexivity. Qed.! ( ) ( 3) October 24, / 47
26 app : l1, l2, l3 (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) : l1 l1 = [] ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3) ++ ( ) ( 3) October 24, / 47
27 l1 = n::l1 (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) ((n::l1 ) ++ l2) ++ l3 = (n::l1 ) ++ (l2 ++ l3) ++ n::((l1 ++ l2) ++ l3) = n::(l1 ++ (l2 ++ l3)) ( ) ( ) ( 3) October 24, / 47
28 : n P(n) : n n = 0 : P(0) n = S(n ) P(n ) : P(S(n )) ( ) ( ) ( 3) October 24, / 47
29 : l P(l) : l l = [] : P([]) l = n::l P(l ) : P(n::l ) ( ) ( ) ( 3) October 24, / 47
30 : Fixpoint rev (l:natlist) : natlist := match l with nil => nil h :: t => rev t ++ [h] end. append ( ) ( 3) October 24, / 47
31 Theorem rev_length_firsttry : forall l : natlist, length (rev l) = length l. Proof. intros l. induction l as [ n l ]. - (* l = [] *) reflexivity. - (* l = n :: l *) simpl. (* : length (rev l ++ n) = S (length l ) *) append length! ( ) ( 3) October 24, / 47
32 Theorem app_length : forall l1 l2 : natlist, length (l1 ++ l2) = (length l1) + (length l2). Proof. intros l1 l2. induction l1 as [ n l1 ]. - (* l1 = nil *) reflexivity. - (* l1 = cons n l1 *) simpl. rewrite -> IHl1. reflexivity. Qed. ( ) ( ) ( 3) October 24, / 47
33 ! Theorem rev_length : forall l : natlist, length (rev l) = length l. Proof. intros l. induction l as [ n l ]. - (* l = nil *) reflexivity. - (* l = cons *) simpl. rewrite -> app_length, plus_comm. simpl. rewrite -> IHl. reflexivity. Qed. rewrite ( ) ( 3) October 24, / 47
34 ( 1) : l1, l2 length (l1 ++ l2) = length l1 + length l2 : l1 ( length len ) l1 = [] len ([] ++ l2) = length [] + length l2 len, + ( ) ( 3) October 24, / 47
35 l1 = n::l1 length (l1 ++ l2) = len l1 + len l2 len ((n::l1 ) ++ l2) = len (n::l1 ) + len l2 ++, len, + S(len(l1 ++l2)) = S(len l1 + len l2) ( ) ( ) ( 3) October 24, / 47
36 : l length (rev l) = length l : l l = [] length (rev []) = length [] rev, length ( ) ( 3) October 24, / 47
37 + ( ) ( 3) October 24, / 47 l = n::l length (rev l ) = length l length (rev (n::l )) = length (n::l ) rev, length length ((rev l ) ++ [n]) = S (length l ) length (rev l ) + 1 = S (length l )
38 ( 2) : l length (rev l) = length l length (l ++ [n]) = S (length l) ( l ) l l = n::l ( ) ( 3) October 24, / 47
39 : Search! Search foo. foo! proofgeneral C-c C-a C-a C-c C-; ( ) ( 3) October 24, / 47
40 Lists.v ( ) ( ) ( ) ( 3) October 24, / 47
41 Inductive natoption : Type := Some : nat -> natoption None : natoption. Some 5 Some 42 None. ( ) ( 3) October 24, / 47
42 n nth n Fixpoint nth_bad (n:nat) (l:natlist) : nat := match l with nil => 42 (* arbitrary! *) a :: l => match beq_nat n O with true => a false => nth_bad (pred n) l end end. ( ) ( 3) October 24, / 47
43 Some None Fixpoint nth_error (l:natlist) (n:nat) : natoption := match l with nil => None a :: l => match beq_nat n O with true => Some a false => nth_error l (pred n) end end. ( ) ( 3) October 24, / 47
44 : if then else... a :: l => if beq_nat n O then Some a else nth_error l (pred n)... bool inductive type! then else ( ) ( 3) October 24, / 47
45 Lists.v ( ) ( ) partial maps, dictionary, (association list) ( ) ( 3) October 24, / 47
46 11/ 10:30 Exercise: snd_fst_is_swap (1), list_funs (2), list_exercises (3), beq_natlist (2), hd_error (2) Basics.v, Induction.v, Lists.v zip : ( ) (web ) ( ) ( 3) October 24, / 47
47 list_exercises rev_involutive! (!) rev_involutive rev append ( ) ( 3) October 24, / 47
「計算と論理」 Software Foundations その4
Software Foundations 4 cal17@fos.kuis.kyoto-u.ac.jp http://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal/ November 7, 2017 ( ) ( 4) November 7, 2017 1 / 51 Poly.v ( ) ( 4) November 7, 2017 2 / 51 : (
Jacques Garrigue
Jacques Garrigue Garrigue 1 Garrigue 2 $ print_lines () > for i in $1; do > echo $i > done $ print_lines "a b c" a b c Garrigue 3 Emacs Lisp (defun print-lines (lines) (dolist (str lines) (insert str)
I: 2 : 3 +
I: 1 I: 2008 I: 2 : 3 + I: 3, 3700. (ISBN4-00-010352-0) H.P.Barendregt, The lambda calculus: its syntax and semantics, Studies in logic and the foundations of mathematics, v.103, North-Holland, 1984. (ISBN
topics KNOPPIX/Math DVD maxima KSEG GeoGebra Coq 2011 July 17 - Page 1
KNOPPIX/Math ( ) 2011/07/17 topics KNOPPIX/Math DVD maxima KSEG GeoGebra Coq 2011 July 17 - Page 1 (1) 2011 July 17 - Page 2 (2) 2011 July 17 - Page 3 KNOPPIX/Math KNOPPIX: Linux CD/DVD CD/DVD 1 Windows
jssst-ocaml.mgp
Objective Caml Jacques Garrigue Kyoto University garrigue@kurims.kyoto-u.ac.jp Objective Caml? 2 Objective Caml GC() Standard MLHaskell 3 OCaml () OCaml 5 let let x = 1 + 2 ;; val x : int = 3 ;; val-:
Parametric Polymorphism
ML 2 2011/04/19 Parametric Polymorphism Type Polymorphism ? : val hd_int : int list - > int val hd_bool : bool list - > bool val hd_i_x_b : (int * bool) list - > int * bool etc. let hd_int = function (x
Coq/SSReflect/MathComp による定理証明 サンプルページ この本の定価 判型などは, 以下の URL からご覧いただけます. このサンプルページの内容は, 初版 1 刷発行時のものです.
Coq/SSReflect/MathComp による定理証明 サンプルページ この本の定価 判型などは, 以下の URL からご覧いただけます. http://www.morikita.co.jp/books/mid/006241 このサンプルページの内容は, 初版 1 刷発行時のものです. i 1611 400 Coq/SS- Reflect/MathComp 1 1 Coq/SSReflect/MathComp
# let st1 = {name = "Taro Yamada"; id = };; val st1 : student = {name="taro Yamada"; id=123456} { 1 = 1 ;...; n = n } # let string_of_student {n
II 6 / : 2001 11 21 (OCaml ) 1 (field) name id type # type student = {name : string; id : int};; type student = { name : string; id : int; } student {} type = { 1 : 1 ;...; n : n } { 1 = 1 ;...; n = n
koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1
http://www.kb.ecei.tohoku.ac.jp/ koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ 1.1.1 λ, syntax τ (types) ::= b τ 1 τ 2 τ 1 τ 2 M (terms) ::= c τ x M 1 M 2 λx : τ.m (M 1,M 2
ML Edinburgh LCF ML Curry-Howard ML ( ) ( ) ( ) ( ) 1
More Logic More Types ML/OCaml GADT Jacques Garrigue ( ) Jacques Le Normand (Google) Didier Rémy (INRIA) @garriguejej ocamlgadt ML Edinburgh LCF ML Curry-Howard ML ( ) ( ) ( ) ( ) 1 ( ) ML type nebou and
# let rec sigma (f, n) = # if n = 0 then 0 else f n + sigma (f, n-1);; val sigma : (int -> int) * int -> int = <fun> sigma f n ( : * -> * ) sqsum cbsu
II 4 : 2001 11 7 keywords: 1 OCaml OCaml (first-class value) (higher-order function) 1.1 1 2 + 2 2 + + n 2 sqsum 1 3 + 2 3 + + n 3 cbsum # let rec sqsum n = # if n = 0 then 0 else n * n + sqsum (n - 1)
Copyright c 2006 Zhenjiang Hu, All Right Reserved.
1 2006 Copyright c 2006 Zhenjiang Hu, All Right Reserved. 2 ( ) 3 (T 1, T 2 ) T 1 T 2 (17.3, 3) :: (Float, Int) (3, 6) :: (Int, Int) (True, (+)) :: (Bool, Int Int Int) 4 (, ) (, ) :: a b (a, b) (,) x y
ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1
2005 sumii@ecei.tohoku.ac.jp 2005 6 24 ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1 let λ 1 let x = e1 in e2 (λx.e 2 )e 1 e 1 x e 2 λ 3 λx.(λy.e)
chapter11.PDF
11. 11.1. 11.1.1. 98 7 15 12 20 158 7/15 12/20 99 11 10 2000 3 31 11/10 3/31 2000 1 141 + 1 = 142 142 2000 3 27 99 12 10 451 344 = 107 2000 1 107 + 1 = 108 108 2000 6 27 98 12 20 98/12/20 99/12/20 2000/6/27
Microsoft PowerPoint - ProD0107.ppt
プログラミング D M 講義資料 教科書 :6 章 中田明夫 nakata@ist.osaka-u.ac.jp 2005/1/7 プログラミング D -M- 1 2005/1/7 プログラミング D -M- 2 リスト 1 リスト : 同じ型の値の並び val h=[10,6,7,8,~8,5,9]; val h = [10,6,7,8,~8,5,9]: int list val g=[1.0,4.5,
VDM-SL VDM VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web bool
VDM-SL VDM++ 23 6 28 VDM-SL Toolbox VDM++ Toolbox 1 VDM-SL VDM++ Web 2 1 3 1.1............................................... 3 1.1.1 bool......................................... 3 1.1.2 real rat int
1. A0 A B A0 A : A1,...,A5 B : B1,...,B
1. A0 A B A0 A : A1,...,A5 B : B1,...,B12 2. 3. 4. 5. A0 A, B Z Z m, n Z m n m, n A m, n B m=n (1) A, B (2) A B = A B = Z/ π : Z Z/ (3) A B Z/ (4) Z/ A, B (5) f : Z Z f(n) = n f = g π g : Z/ Z A, B (6)
1. A0 A B A0 A : A1,...,A5 B : B1,...,B12 2. 5 3. 4. 5. A0 (1) A, B A B f K K A ϕ 1, ϕ 2 f ϕ 1 = f ϕ 2 ϕ 1 = ϕ 2 (2) N A 1, A 2, A 3,... N A n X N n X N, A n N n=1 1 A1 d (d 2) A (, k A k = O), A O. f
4 (induction) (mathematical induction) P P(0) P(x) P(x+1) n P(n) 4.1 (inductive definition) A A (basis ) ( ) A (induction step ) A A (closure ) A clos
4 (induction) (mathematical induction) P P(0) P(x) P(x+1) n P(n) 4.1 (inductive definition) A A (basis ) ( ) A (induction step ) A A (closure ) A closure 81 3 A 3 A x A x + A A ( A. ) 3 closure A N 1,
Programming D 1/15
プログラミング D ML 大阪大学基礎工学部情報科学科中田明夫 nakata@ist.osaka-u.ac.jp 教科書 プログラミング言語 Standard ML 入門 6 章 2005/12/19 プログラミング D -ML- 1 2005/12/19 プログラミング D -ML- 2 補足 : 再帰関数の作り方 例題 : 整数 x,y( ただし x
平成 19 年度 ( 第 29 回 ) 数学入門公開講座テキスト ( 京都大学数理解析研究所, 平成 19 ~8 年月 72 月日開催 30 日 ) 1 PCF (Programming language for Computable Functions) PCF adequacy adequacy
1 PCF (Programming language for Computable Functions) PCF adequacy adequacy 2 N X Y X Y f (x) f x f x y z (( f x) y) z = (( f (x))(y))(z) X Y x e X Y λx. e x x 2 + x + 1 λx. x 2 + x + 1 3 PCF 3.1 PCF PCF
Objective Caml 3.12 Jacques Garrigue ( ) with Alain Frisch (Lexifi), OCaml developper team (INRIA)
Objective Caml 3.12 Jacques Garrigue ( ) http://www.math.nagoya-u.ac.jp/~garrigue/ with Alain Frisch (Lexifi), OCaml developper team (INRIA) Jacques Garrigue Modules in Objective Caml 3.12 1 Objective
Copyright c 2008 Zhenjiang Hu, All Right Reserved.
2008 10 27 Copyright c 2008 Zhenjiang Hu, All Right Reserved. (Bool) True False data Bool = False True Remark: not :: Bool Bool not False = True not True = False (Pattern matching) (Rewriting rules) not
2011.12.3 1 2 Q) A) 3 Q) A) 4 5 6 Haskell 7 8 Parser data Parser a = Parser (String -> [(a,string)]) Parser pwrap :: a -> Parser a pwrap v = Parser $ \inp -> [(v,inp)] Parser pbind :: Parser a -> (a ->
Akito Tsuboi June 22, T ϕ T M M ϕ M M ϕ T ϕ 2 Definition 1 X, Y, Z,... 1
Akito Tsuboi June 22, 2006 1 T ϕ T M M ϕ M M ϕ T ϕ 2 Definition 1 X, Y, Z,... 1 1. X, Y, Z,... 2. A, B (A), (A) (B), (A) (B), (A) (B) Exercise 2 1. (X) (Y ) 2. ((X) (Y )) (Z) 3. (((X) (Y )) (Z)) Exercise
monad.gby
2012.11.18 1 1 2 2 DSL 3 4 Q) A) 5 Q) A) 6 7 8 Haskell 9 10 Parser data Parser a = Parser (String -> [(a,string)]) Parser pwrap :: a -> Parser a pwrap v = Parser $ \inp -> [(v,inp)] Parser pbind :: Parser
org/ghc/ Windows Linux RPM 3.2 GHCi GHC gcc javac ghc GHCi(ghci) GHCi Prelude> GHCi :load file :l file :also file :a file :reload :r :type expr :t exp
3 Haskell Haskell Haskell 1. 2. 3. 4. 5. 1. 2. 3. 4. 5. 6. C Java 3.1 Haskell Haskell GHC (Glasgow Haskell Compiler 1 ) GHC Haskell GHC http://www.haskell. 1 Guarded Horn Clauses III - 1 org/ghc/ Windows
2
2011.11.11 1 2 MapReduce 3 4 5 6 Functional Functional Programming 7 8 9 10 11 12 13 [10, 20, 30, 40, 50] 0 n n 10 * 0 + 20 * 1 + 30 * 2 + 40 * 3 + 50 *4 = 400 14 10 * 0 + 20 * 1 + 30 * 2 + 40 * 3 + 50
haskell.gby
Haskell 1 2 3 Haskell ( ) 4 Haskell Lisper 5 Haskell = Haskell 6 Haskell Haskell... 7 qsort [8,2,5,1] [1,2,5,8] "Hello, " ++ "world!" "Hello, world!" 1 + 2 div 8 2 (+) 1 2 8 div 2 3 4 map even [1,2,3,4]
Microsoft PowerPoint - IntroAlgDs-06-8.ppt
アルゴリズムとデータ構造入門 2006 年 11 月 21 日 アルゴリズムとデータ構造入門 2. データによる抽象の構築 2.2 階層データ構造と閉包性 奥乃博大学院情報学研究科知能情報学専攻知能メディア講座音声メディア分野 http://winnie.kuis.kyoto-u.ac.jp/~okuno/lecture/06/introalgds/ okuno@i.kyoto-u.ac.jp 12
JavaCard p.1/41
JavaCard Email : nagamiya@comp.cs.gunma-u.ac.jp p.1/41 Hoare Java p.2/41 (formal method) (formal specification) (formal) JML, D, VDM, (formal method) p.3/41 Hoare Java p.4/41 (precondition) (postcondition)
RX501NC_LTE Mobile Router取説.indb
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 1 2 3 4 5 6 7 8 19 20 21 22 1 1 23 1 24 25 1 1 26 A 1 B C 27 D 1 E F 28 1 29 1 A A 30 31 2 A B C D E F 32 G 2 H A B C D 33 E 2 F 34 A B C D 2 E 35 2 A B C D 36
論理学入門 講義ノート email: mitsu@abelardfletkeioacjp Copyright c 1995 by the author ll right reserved 1 1 3 2 5 3 7 31 7 32 9 33 13 4 29 41 33 42 38 5 45 51 45 52 47 3 1 19 [ 1] Begin at the beginning [ 2] [
2 Help
BD-HDW63 BD-HDW65 2 Help 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 1 2 3 4 5 6 7 8 9 10 20 21 22 23 24 25 26 27 28 DR 29 30 1 2 4 6 8 5 7 12 31 32 LIVE 33 34 35 36 37 38 39 1 4 7 10 2 5 8 11 3 6 9 12
6 1873 6 6 6 2
140 2012 12 12 140 140 140 140 140 1 6 1873 6 6 6 2 3 4 6 6 19 10 39 5 140 7 262 24 6 50 140 7 13 =1880 8 40 9 108 31 7 1904 20 140 30 10 39 =1906 3 =1914 11 6 12 20 1945.3.10 16 1941 71 13 B29 10 14 14
untitled
20 7 1 22 7 1 1 2 3 7 8 9 10 11 13 14 15 17 18 19 21 22 - 1 - - 2 - - 3 - - 4 - 50 200 50 200-5 - 50 200 50 200 50 200 - 6 - - 7 - () - 8 - (XY) - 9 - 112-10 - - 11 - - 12 - - 13 - - 14 - - 15 - - 16 -
untitled
19 1 19 19 3 8 1 19 1 61 2 479 1965 64 1237 148 1272 58 183 X 1 X 2 12 2 15 A B 5 18 B 29 X 1 12 10 31 A 1 58 Y B 14 1 25 3 31 1 5 5 15 Y B 1 232 Y B 1 4235 14 11 8 5350 2409 X 1 15 10 10 B Y Y 2 X 1 X
3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B
![3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B](/thumbs/102/156825138.jpg "3 3.1 algebraic datatype data k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] B")
3 3.1 algebraic datatype data 1 2... k = 1 1,1... 1,n1 2 2,1... 2,n2... m m,1... m,nm 1 m m m,1,..., m,nm m 1, 2,..., k 1 data Foo x y = Alice x [y] Bob String y Charlie Foo Double Integer Alice 3.14 [1,2],
Microsoft PowerPoint - IntroAlgDs-05-7.ppt
アルゴリズムとデータ構造入門 2005 年 11 月 15 日 アルゴリズムとデータ構造入門 2. データによる抽象の構築 2 Building Abstractions with Data 奥乃 博 具体から抽象へは行けるが 抽象から具体へは行けない ( 畑村洋太郎 直観でわかる数学 岩波書店 ) 1 11 月 15 日 本日のメニュー 2 Building Abstractions with Data
( ) 1 1.5 . Let s. 800g 400ml800g 5 5 5 1 6 4 5 3 3 5 25 5 14 10 50 12 00 3 4.5 3 4.5 3 5 2 3 4 5 25 6 5 9 45 10 15 5 Let s BOX 3 4 5 BOX 25 8 19 4 5 10 45 11 00 3 11 05 11 20 4 3 BOX
xyr x y r x y r u u
xyr x y r x y r u u y a b u a b a b c d e f g u a b c d e g u u e e f yx a b a b a b c a b c a b a b c a b a b c a b c a b c a u xy a b u a b c d a b c d u ar ar a xy u a b c a b c a b p a b a b c a
Condition DAQ condition condition 2 3 XML key value
Condition DAQ condition 2009 6 10 2009 7 2 2009 7 3 2010 8 3 1 2 2 condition 2 3 XML key value 3 4 4 4.1............................. 5 4.2...................... 5 5 6 6 Makefile 7 7 9 7.1 Condition.h.............................
構造化プログラミングと データ抽象
計算の理論 後半第 3 回 λ 計算と型システム 本日の内容 λ 計算の表現力 ( 前回のつづき ) 前回の復習 不動点演算子と再帰 λ 計算の重要な性質 チャーチ ロッサー性 簡約戦略 型付き λ 計算 ブール値 組 ブール値と組の表現 ( 復習 ) true, false を受け取り 対応する要素を返す関数 として表現 T = λt.λf.t F = λt.λf.f if e 1 then e
構造化プログラミングと データ抽象
計算の理論 後半第 3 回 λ 計算と型システム 本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現 不動点演算子と再帰 λ 計算の重要な性質 チャーチ ロッサー性 簡約戦略 型付き λ 計算 ブール値 組 ブール値と組の表現 true, false を受け取り 対応する要素を返す関数 として表現 T = λt.λf.t F = λt.λf.f if e 1 then e 2 else
1. A0 A B A0 A : A1,...,A5 B : B1,...,B
1. A0 A B A0 A : A1,...,A5 B : B1,...,B12 2. 3. 4. 5. A0 A B f : A B 4 (i) f (ii) f (iii) C 2 g, h: C A f g = f h g = h (iv) C 2 g, h: B C g f = h f g = h 4 (1) (i) (iii) (2) (iii) (i) (3) (ii) (iv) (4)
損保ジャパンの現状2011
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 62 63 64 65 66 67 68 69
Microsoft Word - ランチョンプレゼンテーション詳細.doc
PS1-1-1 PS1-1-2 PS1-1-3 PS1-1-4 PS1-1-5 PS1-1-6 PS1-1-7 PS1-1-8 PS1-1-9 1 25 12:4514:18 25 12:4513:15 B PS1-1-10 PS1-2-1 PS1-2-2 PS1-2-3 PS1-2-4 PS1-2-5 PS1-2-6 25 13:1513:36 B PS1-2-7 PS1-3-1 PS1-3-2
記号と準備
tbasic.org * 1 [2017 6 ] 1 2 1.1................................................ 2 1.2................................................ 2 1.3.............................................. 3 2 5 2.1............................................
¥×¥í¥°¥é¥ß¥ó¥°±é½¬I Exercise on Programming I [1zh] ` `%%%`#`&12_`__~~~ alse
![¥×¥í¥°¥é¥ß¥ó¥°±é½¬I Exercise on Programming I [1zh] ` `%%%`#`&12_`__~~~ alse](/thumbs/97/134738565.jpg "¥×¥í¥°¥é¥ß¥ó¥°±é½¬I Exercise on Programming I [1zh] ` `%%%`#`&12_`__~~~ alse")
I Exercise on Programming I http://bit.ly/oitprog1 1, 2 of 14 ( RD S ) I 1, 2 of 14 1 / 44 Ruby Ruby ( RD S ) I 1, 2 of 14 2 / 44 7 5 9 2 9 3 3 2 6 5 1 3 2 5 6 4 7 8 4 5 2 7 9 6 4 7 1 3 ( RD S ) I 1, 2
JA2008
A1 1 10 vs 3 2 1 3 2 0 3 2 10 2 0 0 2 1 0 3 A2 3 11 vs 0 4 4 0 0 0 0 0 3 6 0 1 4 x 11 A3 5 4 vs 5 6 5 1 0 0 3 0 4 6 0 0 1 0 4 5 A4 7 11 vs 2 8 8 2 0 0 0 0 2 7 2 7 0 2 x 11 A5 9 5 vs 3 10 9 4 0 1 0 0 5
: gettoken(1) module P = Printf exception End_of_system (* *) let _ISTREAM = ref stdin let ch = ref ( ) let read () = (let c =!ch in ch := inp
7 OCaml () 1. 2. () (compiler) (interpreter) 2 OCaml (syntax) (BNF,backus normal form ) 1 + 2; let x be 2-1 in x; ::= ; let be in ; ::= + - ::= * / ::= 7.1 ( (printable characters) (tokens) 1 (lexical
fp.gby
1 1 2 2 3 2 4 5 6 7 8 9 10 11 Haskell 12 13 Haskell 14 15 ( ) 16 ) 30 17 static 18 (IORef) 19 20 OK NG 21 Haskell (+) :: Num a => a -> a -> a sort :: Ord a => [a] -> [a] delete :: Eq a => a -> [a] -> [a]
A A A B A B A B A B A B A B A B A B A B A B *1 A B A B A B 1.3 (1.3) A B B A *1 2
Morality mod Science 4 2017 10 19 1 1.1 (1.1) 1 2 A 1, A 2,..., A n B A 1, A 2,..., A n B A 1, A 2,..., A n B A 1, A 2,..., A n B (1.2) 1 A B 2 B A 1.2 A B minao.kukita@gmail.com 1 A A A B A B A B A B
2
Haskell ( ) kazu@iij.ad.jp 1 2 Blub Paul Graham http://practical-scheme.net/trans/beating-the-averages-j.html Blub Blub Blub Blub 3 Haskell Sebastian Sylvan http://www.haskell.org/haskellwiki/why_haskell_matters...
: 1: 3:
1 2013 10 11 google maps engine : : : : : : : : : : 1 4.6.1 2: 1: 3: 4: 6: 5: 7: 2 2.1 2.1.1 2.1.2 2.2 2.2.1 2.2.2 2.2.3 2.2.4 2.2.5 2.3 2.3.1 18 2.3.2 2.3.3 2.3.4 2.3.5 2000 SA 2.3.6 2.4 2.4.1 2.4.2 2.4.3
橡SPA2000.PDF
XSLT ( ) d-oka@is.s.u-tokyo.ac.jp ( ) hagiya@is.s.u-tokyo.ac.jp XSLT(eXtensible Stylesheet Language Transformations) XML XML XSLT XSLT XML XSLT XML XSLT XML XML XPath XML XSLT XPath XML XSLT,XPath 1 XSLT([6])
add1 2 β β - conversion (λx.x + 1(2 β x + 1 x λ f(x, y = 2 x + y 2 λ(x, y.2 x + y 1 λy.2 x + y λx.(λy.2 x + y x λy.2 x + y EXAMPLE (λ(x, y.2
output: 2011,11,10 2.1 λ λ β λ λ - abstraction λ λ - binding 1 add1 + add1(x = x + 1 add1 λx.x + 1 x + 1 add1 function application 2 add1 add1(2 g.yamadatakahiro@gmail.com 1 add1 2 β β - conversion (λx.x
WebIntellTN02.qxp (Page 1)
2004 Check Point Software Technologies Ltd. 1 2004 Check Point Software Technologies Ltd. 2 Webサーバ Webアプリケーション データベース Webアプリケーション データベース 2004 Check Point Software Technologies Ltd. 3 2004 Check Point Software
研究紀要 第５号
3 4 5 6 7 8 a s d f a 9 10 s d a 11 12 s d f g 13 h j a d s 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 a 35 s 36 a 37 s 38 a 39 s 40 a 41 s d 42 f 43 44 46 47 48 49 50 a s d as d 51
SCM (v0201) ( ) SCM 2 SCM 3 SCM SCM 2.1 SCM SCM SCM (1) MS-DOS (2) Microsoft(R) Windows 95 (C)Copyright Microsoft Corp
SCM (v0201) ( ) 14 4 20 1 SCM 2 SCM 3 SCM 4 5 2 SCM 2.1 SCM SCM 2 1 2 SCM (1) MS-DOS (2) Microsoft(R) Windows 95 (C)Copyright Microsoft Corp 1981-1996. 1 (3) C:\WINDOWS>cd.. C:\>cd scm C:\SCM> C:\SCM>
5 IO Haskell return (>>=) Haskell Haskell Haskell 5.1 Util Util (Util: Tiny Imperative Language) 1 UtilErr, UtilST, UtilCont, Haskell C
5 IO Haskell return (>>=) Haskell Haskell Haskell 5.1 Util Util (Util: Tiny Imperative Language) 1 UtilErr, UtilST, UtilCont,... 5.1.1 5.1.2 Haskell C LR ( ) 1 (recursive acronym) PHP, GNU V - 1 5.1.1
PowerPoint Presentation
練習問題 8 の解答例 プログラミング D 大阪大学基礎工学部情報科学科中田明夫 nakata@ist.osaka-u.ac.jp プログラミング D -ML- 1 次の関数の型を推論し その理由を説明せよ fun foo (a,b,c,d:real) = if ab then c else d; 引数 a,b,c,dの型をそれぞれ 'a,'b,'c,'dとおく
情報科学概論 第1回資料
1. Excel (C) Hiroshi Pen Fujimori 1 2. (Excel) 2.1 Excel : 2.2Excel Excel (C) Hiroshi Pen Fujimori 2 256 (IV) :C (C 65536 B4 :2 (2 A3 Excel (C) Hiroshi Pen Fujimori 3 Tips: (1) B3 (2) (*1) (3) (4)Word
Pascal Pascal Free Pascal CPad for Pascal Microsoft Windows OS Pascal
Pascal Pascal Pascal Free Pascal CPad for Pascal Microsoft Windows OS 2010 10 1 Pascal 2 1.1.......................... 2 1.2.................. 2 1.3........................ 3 2 4 2.1................................
B Simon (Trump ) SimonU.pas SimonP.dpr Name FormSimon Caption Position podesktopcenter uses Windows, Messages, SysUtils,
B 132 20 1 1 20.1 20.1.1 1 52 10 1 2 3... 7 8 8 8 20.1.2 1 5 6 7 3 20.1.3 1 3 8 20.1.4 13 20.1.5 4 1 (solitaire) B 133 20.2 20.2.1 Simon (Trump ) SimonU.pas SimonP.dpr 20.2.2 Name FormSimon Caption Position
VBAfiüŒåŁÒver2
Microsoft Excel 1 2 3 4 5 Application.CommandBars("Stop Recording").Visible = True 6 Range("A1").Value = WorksheetFunction.RoundDown(9.27, 0) 7 modorichi = MsgBox(" ",, "") modorichi = MsgBox(prompt:="
1 # include < stdio.h> 2 # include < string.h> 3 4 int main (){ 5 char str [222]; 6 scanf ("%s", str ); 7 int n= strlen ( str ); 8 for ( int i=n -2; i
![1 # include < stdio.h> 2 # include < string.h> 3 4 int main (){ 5 char str [222]; 6 scanf (%s, str ); 7 int n= strlen ( str ); 8 for ( int i=n -2; i](/thumbs/89/99201513.jpg "1 # include < stdio.h> 2 # include < string.h> 3 4 int main (){ 5 char str [222]; 6 scanf (%s, str ); 7 int n= strlen ( str ); 8 for ( int i=n -2; i")
ABC066 / ARC077 writer: nuip 2017 7 1 For International Readers: English editorial starts from page 8. A : ringring a + b b + c a + c a, b, c a + b + c 1 # include < stdio.h> 2 3 int main (){ 4 int a,
r3.dvi
2012 3 / Lisp(2) 2012.4.19 1 Lisp 1.1 Lisp Lisp (1) (setq) (2) (3) setq defun (defun (... &aux...)...) ( ) ( nil ) [1]> (defun sisoku (x y &aux wa sa sho seki) (setq wa (+ x y)) (setq sa (- x y)) (setq
<4D6963726F736F667420576F7264202D2081A193B98BE257656290EA97708CFB8DC08B4B92E88179918D8D878CFB8DC0817A816990568B4B816A81798A6D92E894C5817A2E646F63>
( )
Web Web 1 3 1 21 11 22 23 24 3 2 3 4 5 1 1 11 22 9 2 3 15 11 22 2 11 21 4 5 ( ) 102 ( ) 1 ( 1 2001 Web 1 5 4 1 1 - 7 - [] - 7 10 11 12 12 1 10 1 12 - [] 1 1 2 Q1 Q2 Q3 Q4 Q5 Q6 Q7 Q8 Q9 Q10 3 1 47
夏目小兵衛直克
39(1906)1222 14(1817) 3(1832)1514(1843) 2628 6 (1853) (1854)3727 3(1856) 1 / 13 5(1858)6(1859) 5(1853) () () () () () () 3(1867)29 504111( 2 / 13 )98 23 18 2(1869)310283 100 50() 58 226 3313200982 5033
nenkin.PDF
1 31 1 WEB 10 3,544 429 13 10 22 11 7 WEB 1 2 41.0 15 80.0 20 46.7% 1000 55.8 1000 34.4 21 18.2 1000 23 25 41.0 49.2 29 90.6 42.7 33 56.4% 79.2% 67.4 51.7 37 39 83.7 1 91.0 93.6 9 2 3 1000 96.3 300 1000
-1-
-1- -2- -3-1 8 6% 2 4 6 8 1 48 63 43 6 55 38 78 58 2 88 67 11 22 78 1 56 22 89 47 34 36 32 38 4 34 26 7 -4- 18-5- 3 25 28 (6.%) (6.%) (.9%) 2 15 18 158 1 (3.8%) (56.4%) 5 2 137 27 8 1 68 119 26 71 28 65
2 1/2 1/4 x 1 x 2 x 1, x 2 9 3x 1 + 2x 2 9 (1.1) 1/3 RDA 1 15 x /4 RDA 1 6 x /6 1 x 1 3 x 2 15 x (1.2) (1.3) (1.4) 1 2 (1.5) x 1
1 1 [1] 1.1 1.1. TS 9 1/3 RDA 1/4 RDA 1 1/2 1/4 50 65 3 2 1/15 RDA 2/15 RDA 1/6 RDA 1 1/6 1 1960 2 1/2 1/4 x 1 x 2 x 1, x 2 9 3x 1 + 2x 2 9 (1.1) 1/3 RDA 1 15 x 1 + 2 1/4 RDA 1 6 x 1 1 4 1 1/6 1 x 1 3