2 (concurrency) (sequentiality) cf.

Size: px

Start display at page:

Download "2 (concurrency) (sequentiality) cf."

あきみおおふさ
6 years ago
Views:

2 2 (concurrency) (sequentiality) cf.

3 3

4 4

5 5

6 5

7 6

8 7

9 ? 8 : Yes : No.

10 ? 9 : No. : Yes.

11 10 : C, C++, Lisp,... : cf....

12 11 Concurrent Logic Programming, Concurrent LP Concurrent LP = LP + directionality (of dataflow) = logic + embedded concurrency control cf. Algorithm = Logic + (external) Control (Robert Kowalski, 1979)

13 12 append([],y,y). append([a X],Y,[A Z]) :- append(x,y,z). resolution : :- append(x,y,[p,q,r]). {X=[], Y=[P,Q,R]}, {X=[P], Y=[Q,R]}, {X=[P,Q], Y=[R]}, {X=[P,Q,R], Y=[]}. Yes-No vs.

14 13 P g θ P = gθ gθ P gσ P θ σ θ σ θ

15 14 Y(append([],Y,Y)) X Y Z(append(X,Y,Z) append([a X],Y,[A Z])) = append([p],[q,r],[p,q,r]) {X=[1,2], Y=[3]} {X=[P,Q], Y=[R]}

16 15 :- append(x,y,[p,q,r]) {X=[P], Y=[Q,R]} append(x,y,z) {Z=[P,Q,R]} {X=[P], Y=[Q,R]} nondeterministic

17 1980 Relational Language Concurrent Prolog PARLOG 1985 GHC FCP Flat GHC PARLOG ALPS KL1 Strand 1990 CCP Moded Flat GHC PCN Janus AKL 16 P-Prolog Andorra Prolog CC++ timed CC Oz

18 GHC / KL1 17 cf.»»»»

19 GHC / KL

20 GHC / KL

21 GHC / KL cf. Comm. ACM, March 1993

22 One-Shot Inverter in GHC 21 not(in,out) :- In=0 Out=1. not(in,out) :- In=1 Out=0. In Out Or more concisely: not(0,out) :- true Out=1. not(1,out) :- true Out=0.

23 One-Shot NAND Gate 22 nand(0,y,out) :- true Out=1. nand(x,0,out) :- true Out=1. nand(1,1,out) :- true Out=0. X Out Y Which rule will be selected if both X and Y are 0?

24 Cascaded Inverters 23 :- module main. main :- true not(y,z), not(x,y), tty:ttystream([gett(x),putt([x,y,z]),nl]). not(0,out) :- true Out=1. not(1,out) :- true Out=0. X Y Z

25 More on Inverters 24 Inverter accepting a sequence of input data nots A sequence can be represented as a list. Examples: [0,1,1,0,1] [0,1,1,0,1 A] []

26 More on Inverters 25 nots([], Y ) :- true Y=[]. nots([0 X],Y0) :- true Y0=[1 Y], nots(x,y). nots([1 X],Y0) :- true Y0=[0 Y], nots(x,y). Or, using not, nots([], Y ) :- true Y=[]. nots([a X],Y0) :- true not(a,b), Y0=[B Y], nots(x,y).

27 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none)

28 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none) X=[] Y=[] (none)

29 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none) X=[] Y=[] (none) X=[0,1,1,0,1 X ] Y=[1,0,0,1,0 Y ] nots(x,y )

30 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none) X=[] Y=[] (none) X=[0,1,1,0,1 X ] Y=[1,0,0,1,0 Y ] nots(x,y ) (none) (none) nots(x,y)

31 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none) X=[] Y=[] (none) X=[0,1,1,0,1 X ] Y=[1,0,0,1,0 Y ] nots(x,y ) (none) (none) nots(x,y) X=[2 _] (reduction failure)

32 More on Inverters 26 Behavior of nots(x,y) : Input Output Rest X=[0,1,1,0,1] Y=[1,0,0,1,0] (none) X=[] Y=[] (none) X=[0,1,1,0,1 X ] Y=[1,0,0,1,0 Y ] nots(x,y ) (none) (none) nots(x,y) X=[2 _] X=[0 _], Y=[0 _] (reduction failure) (unification failure)

33 Factorial 27 factorial(x,y) :- X=:=0 Y:=0. factorial(x,y) :- X > 0 X1:=X 1, factorial(x1,y1), Y:=X*Y1. M=5 N=120 factorial(m,n)

34 Factorial 28 factorial(x,y) :- X=:=0 Y:=0. factorial(x,y) :- X > 0 X1:=X 1, factorial(x1,y1), Y:=X*Y1. M=5 N=120 factorial(m,n)

35 Factorial 29 factorial(x,y) :- X=:=0 Y:=0. factorial(x,y) :- X > 0 X1:=X 1, factorial(x1,y1), Y:=X*Y1. M=5 N=120 M1=4 N1=24 M1:=M 1 factorial(m1,n1) N:=M*N1

36 GHC (Guarded Horn Clauses) 30 Concurrent LP = LP + directionality (of dataflow) = logic + embedded concurrency control GHC = Horn Clauses + Guards (algorithm) (logic) (control)

37 GHC 31 h :- G B h : G, B :

38 GHC 32 h :- G B h : G, B : G : B : true

39 GHC 33 :- B KLIC main main

40 34 X X=f(Y) X=f(5) X X=1 X=2

41 35 t 1 = t 2»»»

42 36»

43 37 main :- true not(x,y), not(1,x). main :- true not(x,y), not(y,x).

44 38 main :- true not(1,x), not(2,y). 1=2 cf. main :- true not(0,x), not(1,x).

45 append 39 :- module main. main :- true append([1,2,3],[4,5],x). append([], Y,Z ) :- true Y=Z. append([a X],Y,Z0) :- true Z0=[A Z], append(x,y,z). cf. Prolog append([], Y,Y ). append([a X],Y,[A Z]) :- append(x,y,z).

46 length 40 length([], N) :- true N:=0. length([_ L0],N) :- true length(l0,n0), N:=N0+1. length(l,n) :- true length(l,0,n). length([], N0,N) :- true N:=N0. length([_ L0],N0,N) :- true N1:=N0+1, length(l0,n1,n).

47 list reversal 41 nreverse([], Lr) :- true Lr=[]. nreverse([a L0],Lr) :- true nreverse(l0,lr0), append(lr0,[a],lr). reverse(l,lr) :- true reverse(l,[],lr). reverse([], S,Lr) :- true Lr=S. reverse([a L],S,Lr) :- true reverse(l,[a S],Lr).

48 insertion sort 42 sort([], S) :- true S=[]. sort([x L0],S) :- true sort(l0,s0), insert(x,s0,s). insert(x,[], R) :- true R=[X]. insert(x,[y L], R) :- X=<Y R=[X,Y L]. insert(x,[y L0],R) :- X > Y R=[Y L], insert(x,l0,l).

49 insertion sort 43 sort([], S) :- true S=[]. sort([x L0],S) :- true sort(l0,s0), insert([x],s0,s). insert([x],[], R) :- true R=[X]. insert([x],[y L], R) :- X=<Y R=[X,Y L]. insert([x],[y L0],R) :- X > Y R=[Y L], insert([x],l0,l).

50 44 call by value»»

51 45

52 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns

53 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ]

54 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ns=[1 Ns ]

55 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ns=[1 Ns ] Ms =[2 Ms ]

56 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ms =[2 Ms ] Ns=[1 Ns ] Ns =[3 Ns ]

57 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ms =[2 Ms ] Ns=[1 Ns ] Ns =[3 Ns ] Ms =[3 Ms ]

58 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ms =[2 Ms ] Ms =[3 Ms ] Ns=[1 Ns ] Ns =[3 Ns ] Ns =[6 Ns ]

59 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ms =[2 Ms ] Ms =[3 Ms ] Ns=[1 Ns ] Ns =[3 Ns ] Ns =[6 Ns ] Ms =[4 Ms ]

60 Prefix Sum 46 gen(100,ms) Ms sum(ms,ns) Ns Ms=[1 Ms ] Ms =[2 Ms ] Ms =[3 Ms ] Ms =[4 Ms ] Ns=[1 Ns ] Ns =[3 Ns ] Ns =[6 Ns ] Ns =[10 Ns ]

61 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os)

62 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300

63 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ]

64 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Os=[putt(2),nl Os ]

65 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Os=[putt(2),nl Os ]

66 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Os=[putt(2),nl Os ] Os =[putt(3),nl Os ]

67 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Ps =[5 Ps ] Os=[putt(2),nl Os ] Os =[putt(3),nl Os ]

68 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Ps =[5 Ps ] Os=[putt(2),nl Os ] Os =[putt(3),nl Os ] Os =[putt(5),nl Os ]

69 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Ps =[5 Ps ] Ps =[7 Ps ] Os=[putt(2),nl Os ] Os =[putt(3),nl Os ] Os =[putt(5),nl Os ]

70 Printing Prime Numbers 47 primes(max,ps) Ps outconv(ps,os) Os ttystream(os) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Ps =[5 Ps ] Ps =[7 Ps ] Os=[putt(2),nl Os ] Os =[putt(3),nl Os ] Os =[putt(5),nl Os ] Os =[putt(7),nl Os ]

71 Twin Primes 48 primes(max,ps) Ps twins(ps,ts) Ts Max=300 Generate a stream of twin primes up to a given number. (cf. differential programming) Ts=[twin(3,5) Ts ] Ts =[twin(5,7) Ts ] Ts =[twin(11,13) Ts ] Ts =[twin(17,19) Ts ]

72 Hamming s Problem 49 Generate an ascending sequence of natural numbers ( 1000) of the form 2 l 3 m 5 n (l, m, n 0). Do not use integer division.

73 GHC 50 (ask) (tell)

74 GHC 51

75 Prolog vs. GHC 52 Prolog LP GHC Concurrent LP

76 Tranformational vs. Reactive 53 deterministic transformational Prolog nondeterministic transformational GHC / KL1 indeterminacy reactive

77 Tranformational vs. Reactive 54 Transformational one transaction Reactive possibly many tranactions input may depend on output

78 55 primes(max,ps) Ps client(ps,...) Max=300 Ps=[2 Ps ] Ps =[3 Ps ] Ps =[5 Ps ] Ps (62) =[]

79 56 primes(max,ps) Ps client(ps,...) P=2 P =3 P =5 Ps=[P Ps ] Ps =[P Ps ] Ps =[P Ps ] P (61) =293 Ps (62) =[]

80 57 [0,1,1,2,3,5,8,...] fiblazy(ns) :- true fiblazy(,,ns). fiblazy(_, _, []) :- true true. fiblazy(n1,n2,[n3 Ns1]) :- true N3:=N1+N2, fiblazy(n2,n3,ns1).

81 58 counter(s) :- true counter(s,0). counter([],c) :- true true. counter([up(n) S],C0) :- true C:=C0+N, counter(s,c). counter([reset S],C) :- true counter(s,0). counter([show(v) S],C) :- true V:=C, counter(s,c).

82 59 up(n): N show(v): V

83 60 tty:ttystream(s) putc(c) nl putt(t) fwrite(s) getc(c) unget(c) gett(t) C T S C C T

84 61 merge([], Ys, Zs) :- true Zs=Ys. merge(xs, [], Zs) :- true Zs=Xs. merge([a Xs],Ys, Zs0) :- true Zs0=[A Zs], merge(xs,ys,zs). merge(xs, [A Ys],Zs0) :- true Zs0=[A Zs], merge(xs,ys,zs).

85 (difference lists) 62 L 1 x 1,..., x n (n 0) L 2 L 1 L 2 cf. time vs. duration, position vs. displacement x 1,..., x n x 1,..., x n? L 1 L 2 L 1 L 2

86 (difference lists) 63 L 2 (L 1,L 2 )

87 Quicksort 64 qsort(xs,ys) :- true qsort(xs,ys,[]). qsort([], Ys0,Ys ) :- true Ys=Ys0. qsort([x Xs],Ys0,Ys3) :- true part(x,xs,s,l), qsort(s,ys0,[x Ys2]), qsort(l,ys2,ys3). part(_,[], S, L ) :- true S=[], L=[]. part(a,[x Xs],S0,L ) :- A>=X S0=[X S], part(a,xs,s,l). part(a,[x Xs],S, L0) :- A < X L0=[X L], part(a,xs,s,l).

88 65 cf. Hoare 1978

89 65 cf. Hoare

90 65 cf. Hoare 1978 ins(5) 3 6 8

91 65 cf. Hoare 1978 ins(5) ins(5) 3 6 8

92 65 cf. Hoare 1978 ins(5) ins(5) ins(6) 3 5 8

93 66 cf. Hoare 1978

94 66 cf. Hoare 1978 ins(6) 3 5 8

95 66 cf. Hoare 1978 ins(6) ins(8)

96 66 cf. Hoare 1978 ins(6) ins(8)

97 Element process: n 67 elem([],r,n) :- true R=[ ]. elem([ins(m) L],R0,N) :- M < N R0=[ins(N) R], elem(l,r,m). elem([ins(m) L],R, N) :- M=:=N elem(l,r,n). elem([ins(m) L],R0,N) :- M > N R0=[ins(M) R], elem(l,r,n). elem([has(m,a) L],R, N) :- M < N A=false, elem(l,r,n). elem([has(m,a) L],R, N) :- M=:=N A=true, elem(l,r,n). elem([has(m,a) L],R0,N) :- M > N R0=[has(M,A) R], elem(l,r,n).

98 Terminator process: 68 emptyset([]) :- true true. emptyset([ins(m) L] ) :- true elem(l,r,m), emptyset(r). emptyset([has(m,a) L]) :- true A=false, emptyset(l).

99 69 store g h

100 Reduction of an Inverter 70 nots( A, B) nots([1 P], R) :- true R=[0 B ], nots(p,b ).

101 Reduction of an Inverter 71 A=[1 A ] nots( A, B) nots([1 P], R) :- true R=[0 B ], nots(p,b ).

102 Reduction of an Inverter 72 A=[1 A ] nots([1 A ],B) nots([1 P], R) :- true R=[0 B ], nots(p,b ).

103 Reduction of an Inverter 72 A=[1 A ] nots([1 A ],B) nots([1 P], R) :- true R=[0 B ], nots(p,b ).

104 Reduction of an Inverter 73 A=[1 A ] B=[0 B ] nots(a,b )

105 Reduction of an Inverter 74 A=[1 A ] B=[0 B ] nots(a,b )

106 75 not(a,b)θ (θ ={A [1 A ]}) not([1 P],R) A A B (A=[1 A ] P R(not(A,B)=not([1 P],R))) (Maher, 1987)

107 76 f, g ( ( )) f ( X, K, Xm ) = g( Y1, K, Y 1 n X を含む項 t (X 自身は除く ) に対して t = X ( ( )) 各 n 引数関数 f に対して ( f X, K, X ) = f ( Y, K, Y ) I ( X = Y )) n ( 1 n 1 n i = 1 i i 各 n 引数関数 f に対して I X = Y ) f ( X, K, X ) = ( f ( Y, K, Y )) n i = 1 ( i i 1 n 1 n )

108 77 ( X = X ) X = Y Y = X ( ) X = Y Y = Z X = Z ( ) E E S c E = ( S c)

109 78 E = ( ) S c S c (1) (2) (3) X=s(0) X=s(Y) Y=0 X=0 X=s(0) Y(X=s(Y)) X=s(0) 任意の論理式 E E ( ) = S c が成り立つならば = ( S S c) も成り立つ ( S は任意 )

110 79 c ( S c) ( ) S c false true false maybe yes true no S is inconsistent

111 80 store(x,5) load(x) store(x,6) load(x) X=5 Y=8 Z=3 M

112 81 tell(x=[2 Y]) ask(x=[ ]) tell(y=[3 Z]) ask( A(X=[2 A])) X=[2 Y] Y=[3 Z] Z=[ ] M

113 GHC 82 h :- true B GHC cf. Plotkin, G. D., A Structural Approach to Operational Semantics. DAIMI FN-19, Computer Science Dept., Aarhus Univ., Denmark, 1981.

114 GHC 83 (program) (program clause) (body) (goal) (non-unif. atom) (term) (goal clause) P C B G A T Q ::= set of C s ::= A :- (true) B ::= multiset of G s ::= T 1 =T 2 A ::= p(t 1,..., T n ), p = ::= (as in first-order logic) ::= :- B

115 GHC 84 Configuration: B, C, V B : C : V :» cf. vars(b) vars(c) V :- B 0 initial configuration: B 0, φ, vars(b 0 )

116 85 P c c : P P c c : P1 c1 c1 (if Cond ) P c c 2 2 2

117 86 V C B B C V B B P V C B C V B P,,,,,,,, U U V t t C C V t t P }, {,, }, { = = U (tell)

118 87 (ask + reduction) { h : B} U P { b}, C, V B, C U { b = h}, V U vars( h : B if E = C vars( h) b = h and vars( h : B) IV = ( ( )) )

119 88

120 89 (SIMD) (MIMD) MIMD SIMD MIMD

121 90

122 91

123 91

124 91

125 91» load, store

126 91» load, store»

127 91» load, store»»

128 92 所要時間送信量

129 93»»»»

130 94

131 (scalability) 95?

132 (scalability) 96

133 (scalability) 96 (speedup)

134 (scalability) 96 (speedup) n

135 (scalability) 96 (speedup) n n

136 (scalability) 96 (speedup) n n (efficiency)

137 (scalability) 96 (speedup) n n (efficiency)

138 (scalability) 96 (speedup) n n (efficiency)...

139 (scalability) 96 (speedup) n n (efficiency)... super-linear speedup

140 (scalability) 97 Amdahl p 1 p p

141 AND OR 98

142 AND OR 98 AND

143 AND OR 98 AND OR

144 99

145 99

146 99 cf.

147 99 cf.

148 99 cf.

149 99 cf.

150 GHC KL1 100 GHC KL1

151 GHC KL1 101 OS KL1

152 KL1 102»»

153 KL1 103 OR»»

154 KL1 104 : alternatively : (pragma)

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

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