I: 2 : 3 +

Similar documents
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

…J…−†[†E…n…‘†[…hfi¯„^‚ΛžfiüŒå

Akito Tsuboi June 22, T ϕ T M M ϕ M M ϕ T ϕ 2 Definition 1 X, Y, Z,... 1

koba/class/soft-kiso/ 1 λ if λx.λy.y false 0 λ typed λ-calculus λ λ 1.1 λ λ, syntax τ (types) ::= b τ 1 τ 2 τ 1

平成 19 年度 ( 第 29 回 ) 数学入門公開講座テキスト ( 京都大学数理解析研究所, 平成 19 ~8 年月 72 月日開催 30 日 ) 1 PCF (Programming language for Computable Functions) PCF adequacy adequacy

15 mod 12 = 3, 3 mod 12 = 3, 9 mod 12 = N N 0 x, y x y N x y (mod N) x y N mod N mod N N, x, y N > 0 (1) x x (mod N) (2) x y (mod N) y x

ML λ λ 1 λ 1.1 λ λ λ e (λ ) ::= x ( ) λx.e (λ ) e 1 e 2 ( ) ML λx.e Objective Caml fun x -> e x e let 1

i

I ( ) 1 de Broglie 1 (de Broglie) p λ k h Planck ( Js) p = h λ = k (1) h 2π : Dirac k B Boltzmann ( J/K) T U = 3 2 k BT

³ÎΨÏÀ

40 6 y mx x, y 0, 0 x 0. x,y 0,0 y x + y x 0 mx x + mx m + m m 7 sin y x, x x sin y x x. x sin y x,y 0,0 x 0. 8 x r cos θ y r sin θ x, y 0, 0, r 0. x,

d dt P = d ( ) dv G M vg = F M = F (4.1) dt dt M v G P = M v G F (4.1) d dt H G = M G (4.2) H G M G Z K O I z R R O J x k i O P r! j Y y O -

ii 3.,. 4. F. (), ,,. 8.,. 1. (75%) (25%) =7 20, =7 21 (. ). 1.,, (). 3.,. 1. ().,.,.,.,.,. () (12 )., (), 0. 2., 1., 0,.

() n C + n C + n C + + n C n n (3) n C + n C + n C 4 + n C + n C 3 + n C 5 + (5) (6 ) n C + nc + 3 nc n nc n (7 ) n C + nc + 3 nc n nc n (


1: *2 W, L 2 1 (WWL) 4 5 (WWL) W (WWL) L W (WWL) L L 1 2, 1 4, , 1 4 (cf. [4]) 2: 2 3 * , , = , 1

.....Z...^.[ \..


II No.01 [n/2] [1]H n (x) H n (x) = ( 1) r n! r!(n 2r)! (2x)n 2r. r=0 [2]H n (x) n,, H n ( x) = ( 1) n H n (x). [3] H n (x) = ( 1) n dn x2 e dx n e x2

「計算と論理」 Software Foundations その3

「計算と論理」 Software Foundations その4

III III 2010 PART I 1 Definition 1.1 (, σ-),,,, Borel( ),, (σ-) (M, F, µ), (R, B(R)), (C, B(C)) Borel Definition 1.2 (µ-a.e.), (in µ), (in L 1 (µ)). T

PowerPoint Presentation

ii 3.,. 4. F. ( ), ,,. 8.,. 1. (75% ) (25% ) =7 24, =7 25, =7 26 (. ). 1.,, ( ). 3.,...,.,.,.,.,. ( ) (1 2 )., ( ), 0., 1., 0,.

II A A441 : October 02, 2014 Version : Kawahira, Tomoki TA (Kondo, Hirotaka )

ii 3.,. 4. F. (), ,,. 8.,. 1. (75% ) (25% ) =9 7, =9 8 (. ). 1.,, (). 3.,. 1. ( ).,.,.,.,.,. ( ) (1 2 )., ( ), 0. 2., 1., 0,.

. T ::= x f n t 1 t n F n,m (x(t 1 t n )t 1 t m) x, f n n, F n,m n, m-., F n,m (x(t 1 t n )t 1 t m), x, t 1,..., t n, t 1,..., t m. F n,m (x(t 1 t n )

V 0 = + r pv (H) + qv (T ) = + r ps (H) + qs (T ) = S 0 X n+ (T ) = n S n+ (T ) + ( + r)(x n n S n ) = ( + r)x n + n (d r)s n = ( + r)v n + V n+(h) V

1. A0 A B A0 A : A1,...,A5 B : B1,...,B

W u = u(x, t) u tt = a 2 u xx, a > 0 (1) D := {(x, t) : 0 x l, t 0} u (0, t) = 0, u (l, t) = 0, t 0 (2)

応力とひずみ.ppt

A

newmain.dvi

1 1.1 ( ). z = a + bi, a, b R 0 a, b 0 a 2 + b 2 0 z = a + bi = ( ) a 2 + b 2 a a 2 + b + b 2 a 2 + b i 2 r = a 2 + b 2 θ cos θ = a a 2 + b 2, sin θ =

ii

2016.

第121回関東連合産科婦人科学会総会・学術集会　プログラム・抄録

=

x, y x 3 y xy 3 x 2 y + xy 2 x 3 + y 3 = x 3 y xy 3 x 2 y + xy 2 x 3 + y 3 = 15 xy (x y) (x + y) xy (x y) (x y) ( x 2 + xy + y 2) = 15 (x y)

2011de.dvi

変 位 変位とは 物体中のある点が変形後に 別の点に異動したときの位置の変化で あり ベクトル量である 変位には 物体の変形の他に剛体運動 剛体変位 が含まれている 剛体変位 P(x, y, z) 平行移動と回転 P! (x + u, y + v, z + w) Q(x + d x, y + dy,

応用数学III-4.ppt

PowerPoint Presentation

1.1 1 A

(3) (2),,. ( 20) ( s200103) 0.7 x C,, x 2 + y 2 + ax = 0 a.. D,. D, y C, C (x, y) (y 0) C m. (2) D y = y(x) (x ± y 0), (x, y) D, m, m = 1., D. (x 2 y

I. (CREMONA ) : Cremona [C],., modular form f E f. 1., modular X H 1 (X, Q). modular symbol M-symbol, ( ) modular symbol., notation. H = { z = x

n (1.6) i j=1 1 n a ij x j = b i (1.7) (1.7) (1.4) (1.5) (1.4) (1.7) u, v, w ε x, ε y, ε x, γ yz, γ zx, γ xy (1.8) ε x = u x ε y = v y ε z = w z γ yz

d dt A B C = A B C d dt x = Ax, A 0 B 0 C 0 = mm 0 mm 0 mm AP = PΛ P AP = Λ P A = ΛP P d dt x = P Ax d dt (P x) = Λ(P x) d dt P x =

1.2 y + P (x)y + Q(x)y = 0 (1) y 1 (x), y 2 (x) y 1 (x), y 2 (x) (1) y(x) c 1, c 2 y(x) = c 1 y 1 (x) + c 2 y 2 (x) 3 y 1 (x) y 1 (x) e R P (x)dx y 2

Part () () Γ Part ,



−g”U›ß™ö‡Æ…X…y…N…g…‰

untitled


6kg 1.1m 1.m.1m.1 l λ ϵ λ l + λ l l l dl dl + dλ ϵ dλ dl dl + dλ dl dl 3 1. JIS 1 6kg 1% 66kg 1 13 σ a1 σ m σ a1 σ m σ m σ a1 f f σ a1 σ a1 σ m f 4

DVIOUT

( ) ( ) 1729 (, 2016:17) = = (1) 1 1

I A A441 : April 21, 2014 Version : Kawahira, Tomoki TA (Kondo, Hirotaka ) Google

1. (8) (1) (x + y) + (x + y) = 0 () (x + y ) 5xy = 0 (3) (x y + 3y 3 ) (x 3 + xy ) = 0 (4) x tan y x y + x = 0 (5) x = y + x + y (6) = x + y 1 x y 3 (

応用数学特論.dvi

1 (1) (2)

- 2 -


ＰＲ映画-1

II III I ~ 2 ~

中堅中小企業向け秘密保持マニュアル



入試の軌跡

.1 z = e x +xy y z y 1 1 x 0 1 z x y α β γ z = αx + βy + γ (.1) ax + by + cz = d (.1') a, b, c, d x-y-z (a, b, c). x-y-z 3 (0,

1. A0 A B A0 A : A1,...,A5 B : B1,...,B

II Time-stamp: <05/09/30 17:14:06 waki> ii

n Y 1 (x),..., Y n (x) 1 W (Y 1 (x),..., Y n (x)) 0 W (Y 1 (x),..., Y n (x)) = Y 1 (x)... Y n (x) Y 1(x)... Y n(x) (x)... Y n (n 1) (x) Y (n 1)

1 : f(z = re iθ ) = u(r, θ) + iv(r, θ). (re iθ ) 2 = r 2 e 2iθ = r 2 cos 2θ + ir 2 sin 2θ r f(z = x + iy) = u(x, y) + iv(x, y). (x + iy) 2 = x 2 y 2 +

, 1 ( f n (x))dx d dx ( f n (x)) 1 f n (x)dx d dx f n(x) lim f n (x) = [, 1] x f n (x) = n x x 1 f n (x) = x f n (x) = x 1 x n n f n(x) = [, 1] f n (x

73

6.1 (P (P (P (P (P (P (, P (, P.101

Basic Math. 1 0 [ N Z Q Q c R C] 1, 2, 3,... natural numbers, N Def.(Definition) N (1) 1 N, (2) n N = n +1 N, (3) N (1), (2), n N n N (element). n/ N.

k m m d2 x i dt 2 = f i = kx i (i = 1, 2, 3 or x, y, z) f i σ ij x i e ij = 2.1 Hooke s law and elastic constants (a) x i (2.1) k m σ A σ σ σ σ f i x

ax 2 + bx + c = n 8 (n ) a n x n + a n 1 x n a 1 x + a 0 = 0 ( a n, a n 1,, a 1, a 0 a n 0) n n ( ) ( ) ax 3 + bx 2 + cx + d = 0 4

ii 2. F. ( ), ,,. 5. G., L., D. ( ) ( ), 2005.,. 6.,,. 7.,. 8. ( ), , (20 ). 1. (75% ) (25% ). 60.,. 2. =8 5, =8 4 (. 1.) 1.,,

1 No.1 5 C 1 I III F 1 F 2 F 1 F 2 2 Φ 2 (t) = Φ 1 (t) Φ 1 (t t). = Φ 1(t) t = ( 1.5e 0.5t 2.4e 4t 2e 10t ) τ < 0 t > τ Φ 2 (t) < 0 lim t Φ 2 (t) = 0

基礎数学I

x (x, ) x y (, y) iy x y z = x + iy (x, y) (r, θ) r = x + y, θ = tan ( y ), π < θ π x r = z, θ = arg z z = x + iy = r cos θ + ir sin θ = r(cos θ + i s

x () g(x) = f(t) dt f(x), F (x) 3x () g(x) g (x) f(x), F (x) (3) h(x) = x 3x tf(t) dt.9 = {(x, y) ; x, y, x + y } f(x, y) = xy( x y). h (x) f(x), F (x

Jacques Garrigue

Int Int 29 print Int fmt tostring 2 2 [19] ML ML [19] ML Emacs Standard ML M M ::= x c λx.m M M let x = M in M end (M) x c λx.

1 n A a 11 a 1n A =.. a m1 a mn Ax = λx (1) x n λ (eigenvalue problem) x = 0 ( x 0 ) λ A ( ) λ Ax = λx x Ax = λx y T A = λy T x Ax = λx cx ( 1) 1.1 Th

i 18 2H 2 + O 2 2H 2 + ( ) 3K

6.1 (P (P (P (P (P (P (, P (, P.

I, II 1, A = A 4 : 6 = max{ A, } A A 10 10%

(iii) 0 V, x V, x + 0 = x. 0. (iv) x V, y V, x + y = 0., y x, y = x. (v) 1x = x. (vii) (α + β)x = αx + βx. (viii) (αβ)x = α(βx)., V, C.,,., (1)

1 (1) ( i ) 60 (ii) 75 (iii) 315 (2) π ( i ) (ii) π (iii) 7 12 π ( (3) r, AOB = θ 0 < θ < π ) OAB A 2 OB P ( AB ) < ( AP ) (4) 0 < θ < π 2 sin θ

December 28, 2018

x = a 1 f (a r, a + r) f(a) r a f f(a) 2 2. (a, b) 2 f (a, b) r f(a, b) r (a, b) f f(a, b)

( ; ) C. H. Scholz, The Mechanics of Earthquakes and Faulting : - ( ) σ = σ t sin 2π(r a) λ dσ d(r a) =

¿ô³Ø³Ø½øÏÀ¥Î¡¼¥È

Lebesgue可測性に関するSoloayの定理と実数の集合の正則性=1This slide is available on ` `%%%`#`&12_`__~~~ౡ氀猀e

.3. (x, x = (, u = = 4 (, x x = 4 x, x 0 x = 0 x = 4 x.4. ( z + z = 8 z, z 0 (z, z = (0, 8, (,, (8, 0 3 (0, 8, (,, (8, 0 z = z 4 z (g f(x = g(

Transcription:

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 044487 5085). - 24 1991 3500. (ISBN 4-7649-0184-6)

I: 4 Turing

I: 5

I: 6 1930 Church 1950 McCarthy Lisp 1960 Landin Algol60 1970 Scott 1970 : ML, Haskell

I: 7 : λx.x + 1 λx.(λy.x + y) : (λx.x + 1) 5 5 + 1

I: 8 Definition 1 ( ) V Λ (1) (3) (1) x V x Λ ( ) (2) M, N Λ (MN) Λ ( ) (3) M Λ, x V (λx.m) Λ ( ) < > ::= < > (< > < >) ( < >. < >)

I: 9 : (λx.(λy.(x y))) (λ.(x y)) x ((x y) z) (λx.(x.y)) ((λx.(x x)) (λx.(x x))) (x (λy.z)) (y (λy))

I: 10. ((λx.(x x)) (λx.(x x))) (λx.(x x))(λx.(x x)). ((... (M 1 M 2 )...) M n ) M 1 M 2... M n. (λx 1.(... (λx n.m)...)) λx 1... x n.m

I: 11 (λx.(λy.((x y) (z u))))

I: 12 Definition 2 ( ) 1. x V x. 2. (M N) M N (M N) 3. (λx.m) M (λx.m) M M (M M M M : (λx y.x) (λy.x) z

I: 13 : x (ϵ) : ap (ϵ) (1) (2) M 1 M 2 : λx (ϵ) (1) M 1

I: 14 (1 1 2). ϵ ϵ i = i ϵ (λx y.x) (λy.x) z ap (ϵ) ap (1) z (2) λx (1 1) λy (1 2) λy (1 1 1) x (1 2 1) x (1 1 1 1)

I: 15 Definition 3 ( ) M Λ O(M) 1. M = x O(M) = {ϵ} 2. M = M 1 M 2 O(M) = {ϵ} {i u u O(M i ), i = 1, 2} 3. M = λx.m 1 O(M) = {ϵ} {1 u u O(M 1 )}

I: 16 M/u: u O(M) M/ϵ = M (M 1 M 2 )/i u = M i /u, { i=1,2 } (λx.m 1 )/1 u = M 1 /u u v: v u u v = def w, v = u w

I: 17 Definition 4 ( ) M x u O(M), M/u = x M v O(M), [v < u M/v / λx.(m/v 1)] Definition 5 ( ) M x u O(M), M/u = x M v O(M), [v < u M/v λx.(m/v 1)]

I: 18 (λx y.x) (λy.x) z ap (ϵ) ap (1) z (2) λx (1 1) λy (1 2) λy (1 1 1) x (1 2 1) x (1 1 1 1) : M FV(M)

I: 19 λx.m f(x) = M f(x) = x + 5 f(y) = y + 5 f λx.m λy.m M M x y M M[x := y] λx.x λy.y λx.plus x x λy.plus y y

I: 20 M[x := N]: M M x N { N if x y y[x := N] y otherwise (M 1 M 2 )[x := N] M 1 [x := N] M 2 [x := N] (λy.m 1 )[x := N] λy.m 1 [x := N] if y / x y /FV(N) (by renaming) N M : (λy.x y)[x := λw.y w]

I: 21 Lemma 1 ( ) L, M, N Λ x / y x /FV(L) M[x := N][y := L] M[y := L][x := N[y := L]]

I: 22 M M = x. LHS = x[x := N][y := L] = N[y := L] RHS = x[y := L][x := N[y := L]] = x[x := N[y := L]] = N[y := L]

I: 23 M = y. LHS = y[x := N][y := L] = y[y := L] = L RHS = y[y := L][x := N[y := L]] = L[x := N[y := L]] { x /FV(L) } = L

I: 24 M = z, z x z y. LHS = z[x := N][y := L] = z[y := L] = z RHS = z[y := L][x := N[y := L]] = z[x := N[y := L]] = z

I: 25 M = (M 1 M 2 ). LHS = (M 1 M 2 )[x := N][y := L] = (M 1 [x := N] M 2 [x := N])[y := L] = M 1 [x := N][y := L] M 2 [x := N][y := L] = { inductive hypothesis } M 1 [y := L][x := N[y := L]] M 2 [y := L][x := N[y := L]] = (M 1 [y := L] M 2 [y := L])[x := N[y := L]] = (M 1 M 2 )[y := L][x := N[y := L]] = RHS

I: 26 M = λz.m, z x z y. LHS = (λz.m )[x := N][y := L] = (λz.m [x := N])[y := L] = λz.m [x := N][y := L] = { inductive hypothesis } λz.m [y := L][x := N[y := L]] = (λz.m [y := L])[x := N[y := L]] = (λz.m )[y := L][x := N[y := L]] = RHS

I: 27 Definition 6 ( ) (combinator) I λx.x K λx y.x F λx y.y S λx y z.x z (y z) B λx y z.x (y z) C λx y z.x z y Q (λx.x x) (λx.x x)

I: 28 β Λ Definition 7 (β ) 1. Λ β β = {< (λx.p )Q, P [x := Q] > P, Q Λ} 2. β 1 β β (a) < M, N > β M β N (b) M β N L Λ, x V, L M β L N M L β N L λx.m β λx.n.

I: 29 : II (λx.x) I β I KI(II) (λx y.x)i(ii) β β (λy.i)(ii) I SKK β

I: 30 Lemma 2 ( (compatibility)) u O(M), N 1 β N 2 M[u N 1 ] β M[u N 2 ] β : β 0

I: 31 R (i) a R a (ii) a R b b R a (iii) a R b, b R c a R c

I: 32 Definition 8 ( = β ) = β Λ L, M, N 1. M β N M = β N 2. M = β N N = β M 3. M = β N N = β L M = β L = β

I: 33 Definition 9 (β (β-redex)) P, Q (λx. P ) Q (β-redex) : (λx.x y) z w Definition 10 (β ) β β : z y w

I: 34 Definition 11 ( ) M = β N N β M β : b (λx. x y) z w Ω (λx. x x) (λx. x x) K I Ω

I: 35 Church-Rosser Theorem 3 (Church-Rosser, CR ) M, N Λ.[M = β N L Λ.[M β L N β L]] M = β N β β L

I: 36 Corollary 4 β N 1, N 2 N 1 N 2 N 1 = β N 2 CR L Λ.[N 1 β L N 2 β L] N 1 N 2

I: 37 (Congrence) Definition 12 ( ) M, M 1, M 2 Λ, M β M 1 M β M 2 M 3 Λ, M 1 β M 3 M 2 β M 3 ]

I: 38 Theorem 5 β CR β [ ] ( ) : M, M 1, M 2 Λ, M β M 1 M β M 2 = β M = β M 1 M = β M 2 M 1 = β M 2 CR M 3 Λ, M 1 β M 3 M 2 β M 3. ( ) : M = β N 1. M β N M = β N 2. N = β M M = β N 3. M = β N N = β N M = β N

I: 39

I: 40 x ((λu v w. u w (v w)) (I x) (I (I I)) z) = x ((λv w. (I x) w (v w)) (I (I I)) z) = x ((λw. (I x) w ((I (I I)) w)) z) = x ((I x) z ((I (I I)) z)) = x (x z ((I (I I)) z)) = x (x z ((I I) z)) = x (x z (I z)) = x (x z z)

I: 41 Definition 13 ( ) β M Theorem 6

I: 42 true λt f. t false λt f. f test λl m n. l m n and λb c. test b c false or λb c. test b true c and true true = β true

I: 43 pair λf s b. b f s fst λp. p true snd λp. p false fst (pair v w) = β v

I: 44 Church numbers: 0 λs z. z 1 λs z. s z n λs z. s (s... (s z)...) succ λn s z. s (n s z) plus λm n s z. m s (n s z) times λm n. m (plus n) 0 exp λm n. n m

I: 45 5 12 1 M[x := N][x := L] M[x := N[x := L]] 2 (λx y. (λl w. w w) x y) (S a) (K I) β 3 snd (pair v w) = β w 4 fix f (λx.f(x x))(λx.f(x x)) fix f = β f(fix f)

2024 © docsplayer.net プライバシー | 利用規約 | フィードバック