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 PCF (call-by-value) PCF (call-by-name) PCF M, N, L PCF
PCF ( ) PCF PCF 1. PCF 0, 1, 2, ( PCF ) PCF succ M, pred M M 1 / pred 0 succ (succ 5) 7 PCF succ pred 2 ( ) 2. x, y, z, x 5 pred x 4 3. PCF 0 ifzero L then M else N L 0 M N ifzero (pred x) then M else N x 0 1 M N 4. PCF fun(x : τ). M x M 1 x M 1 M
PCF y 7 fun(x : τ). succ y y 7 x succ y ( 8 ) y 8 τ x τ nat 5. (M N) M 1 M 2 M n (( (M 1 M 2 ) ) M n ) N M M N (fun(x : nat). pred x) (succ 3) ( L ) (a) succ 3 4 (b) fun(x : nat). pred x pred V (c) V 4 4 x pred x 3 L 6. PCF rec f (x : τ) : τ. M fun(x : τ). M x M x M M f Dbl rec dbl(x : nat) : nat. ifzero x then 0 else succ (succ (dbl (pred x))) n n 0 0 n 0 (dbl ) Dbl n 1 2 n Dbl n 2n
M N M N (= ) (call-by-value) (call-by-name) (Algol, Haskell ) PCF PCF 0, 1, 2, 0, 1, 2, succ M, pred M x ifzero L then M else N fun(x : τ). M M N rec f (x : τ) : τ. M M 1 / x L 0 M N x M M N M f 1: PCF PCF F = fun(x : nat). fun(y : nat). M m, n F m n 1 PCF add = fun(x : nat). rec l(y : nat) : nat. ifzero y then x else succ (l (pred y)) sub = fun(x : nat). rec l(y : nat) : nat. ifzero y then x else pred (l (pred y)) mul = fun(x : nat). rec l(y : nat) : nat. ifzero y then 0 else add x (l (pred y)) PCF ( ) 3.2 PCF L x ( L ) M x L fun(x : τ). M rec f (x : τ) : τ. M rec x(y : τ) : τ. M
L x x L fun(x : τ). M x rec f (x : τ) : τ. M f x M FV(M) M FV(M) = M FV(M) M fun(x : nat). succ (succ x) fun(y : nat). succ (succ y) α M x x z M[z/x] ((fun(x : nat). x) x)[z/x] = (fun(x : nat). x) z fun(x : τ). M α fun(z : τ). M[z/x] (z FV(M)) rec f (x : τ) : τ. M α rec f (z : τ) : τ. M[z/x] (z FV(M) { f }) rec x(y : τ) : τ. M α rec z(y : τ) : τ. M[z/x] (z FV(M) {y}) α = α α 2 M = α N M, N Barendregt variable convention (BVC) M 1,, M n M i (1 i n) x x M 1,, M n M 1,, M n ( ) M 1,, M n BVC M 1,, M n M i = α M i (1 i n) BVC 3.3 PCF PCF succ (fun(x : nat). x) fun(x : nat). x 1 1. nat 2. τ τ (τ τ ) τ 1 τ n 1 τ n (τ 1 ( (τ n 1 τ n ) )) 2 R (M, N) R C[ ] (C[M], C[N]) R C[M], C[N] C[ ] M, N
PCF nat (nat nat) (nat nat) nat x : τ Γ x : τ Γ x : τ Γ Γ M : τ ( ) Γ M τ : Y 1 Y n X Y 1 Y n X Γ n : nat x : τ Γ Γ x : τ Γ M : nat Γ succ M : nat Γ M : nat Γ pred M : nat Γ, x : τ M : τ Γ M : τ τ Γ N : τ Γ fun(x : τ). M : τ τ Γ M N : τ Γ L : nat Γ M : τ Γ N : τ Γ ifzero L then M else N : τ Γ, f : τ τ, x : τ M : τ Γ rec f (x : τ) : τ. M : τ τ Γ M : τ Γ M : τ (fun(x : nat). x) (succ 3) : nat x : nat x : nat x : nat x : nat fun(x : nat). x : nat nat 3 : nat succ 3 : nat (fun(x : nat). x) (succ 3) : nat PCF 3.1 Γ M τ, τ Γ M : τ Γ M : τ τ = τ 3.2 Γ M : τ τ Γ x Γ, x : τ M : τ
x 1 : τ 1,, x n : τ n M : τ N i : τ i (1 i n) M x i N i M[N 1 /x 1,, N n /x n ] 3 3.3 M[N 1 /x 1,, N n /x n ] : τ 4 PCF 3.1 PCF 0, 1, 2, fun(x : τ). M τ C τ C τ = {V V : τ V } M V M V n n M n succ M n + 1 L 0 M V ifzero L then M else N V M 0 pred M 0 fun(x : τ). M fun(x : τ). M M n n 1 pred M n 1 L k N V k 0 ifzero L then M else N V M fun(x : τ). M N W M [W/x] V M N V rec f (x : τ) : τ. M fun(x : τ). M[rec f (x : τ) : τ. M/ f ] M V V M V M big-step semantics 1 small-step semantics Dbl 2 Dbl fun(x : nat). ifzero x then 0 else succ (succ (Dbl (pred x))) W n N B n B n = ifzero n then 0 else succ (succ (Dbl (pred n))) 3 BVC BVC α
B 0 0 Dbl 2 4 Dbl W 2 2 2 2 Dbl 2 4 Dbl W 2 2 pred 2 1 1 1 Dbl (pred 2) 2 succ (Dbl (pred 2)) 3 Dbl W succ (succ (Dbl (pred 2))) 4 B 2 4 1 1 pred 1 0 Dbl (pred 1) 0 succ (Dbl (pred 1)) 1.. B 0 0 succ (succ (Dbl (pred 1))) 2 B 1 2 4.1 1. V V V 2. M M V V 3. M V, V M V M V V = V 4. M : τ V M V V : τ M 1. M V V M succ (fun(x : τ). M) 2. M V M Ω = (rec f (x : nat) : nat. f x) Ω 0 : nat Ω 0 1 2 error succ M fun(x : τ). M succ M error M error succ M error M M error M M error ( ) M : τ M V V error
4 M M ( 2) 5 PCF PCF ( ) 1. τ [[τ]] [[x 1 : τ 1,, x n : τ n ]] = [[τ 1 ]] [[τ n ]] 1 { } 2. Γ M : τ [[M]] [[Γ]] [[τ]] Γ M [[τ]] PCF 5 [[nat]] = N, [[τ τ ]] = [[τ]] [[τ ]] 1. PCF M : nat M 2. rec f (x : nat) : M. : nat nat f M N N f M x N f M (x) = [[M]]( f M, x) (1) P M (N N) (N N) (1) P M = λh. λx. [[M]](h, x) f M = P M ( f M ) 4 ;? 5 PCF rec PCF
rec f (x : τ) : M. f M P M N N ( / ) f M ( 2 ) Scott PCF 5.1 5.1 1. D D D (D, D ) ( ) d D. d D d ( ) d, d, d D. d D d d D d = d D d ( ) d, d D. d D d d D d = d = d 2. ω- (ω-complete partial order ω-cpo) (D, D ) d 0 D d 1 D n N d n 3. ω- (ω-complete pointed partial order ω-cppo) ω-cpo (D, D ) D 6 D ω-cpo (ω-cppo) D D ( D ) ω-cpo 1. X = X (X, = X ) ω-cpo 2. X P(X) ω-cppo d 0 d 1 i N d i 3. { } ω-cppo Sierpinski space O 4. N N { } ω-cppo ω 0 1 2 ω-cpo 5.2 D, D ω-cpo 6 ω-cpo predomain ω-cppo domain
1. f D D f D x, y D x D y = f (x) D f (y) 2. f D D f D d 0 D d 1 D D f d n = f (d n ) n N D D [D D ] k N ω O x k δ k (x) = x < k n N δ 5.2 ω-cpo D, D ω-cpo D D (d, d ) D D (e, e ) d D e d D e (D D, D D ) ω-cpo D D 5.3 D, D, D ω-cpo 1. f [D D ], g [D D ] λx. ( f (x), g(x)) [D D D ] 2. π D D D, π D D D π(x, y) = x, π (x, y) = y π [D D D], π [D D D ]
D, D ω-cpo [D D ] f [D D ] g x D. f (x) D g(x) ([D D ], [D D ]) ω-cpo [D D ] 5.4 D, D, D ω-cpo 1. f [D D D ] λ( f ) D (D D ) f λ( f )(x) = λy. f (x, y) λ( f ) [D [D D ]] 2. ev ((D D ) D) D ev( f, x) = f (x) ev [[D D ] D D ] D ω-cpo D ω-cppo [D D ] ω-cppo D ω-cpo D D { } D x D y x = x D y (D { }, D ) ω-cppo D D D ( ) 5.5 D, D ω-cpo seq [D [D D ] D ] seq(, f ) =, seq( x, f ) = f (x) let e D e x D D let x be e in e seq(e, λx. e ) 5.3 5 ω-cppo 5.6 D ω-cppo f [D D]
1. D f ( D ) f ( f ( D )) f (n) ( D ) f (n) ( D ) f n N 2. fix : f n N f (n) ( D ) [D D] D ( fix [[D D] D]) 5.4 PCF PCF τ ω-cpo [[τ]] [[nat]] = (N, = N ), [[τ τ ]] = [[[τ]] [[τ ]] ] [[x 1 : τ 1,, x n : τ n ]] = [[τ 1 ]] [[τ n ]] { } Γ M : τ [[M]] [[[Γ]] [[τ]] ] [[τ]] M Γ [[M]] [[τ]] Γ i x i ρ (v 1,, v n ) [[x i ]] = λ(v 1,, v n ). v i (n Γ ) [[n]] = λρ. n [[fun(x : τ). M]] = λρ. λx. [[M]](ρ, x) [[M N]] = λρ. let n be [[N]]ρ in let m be [[M]]ρ in ev(m, n) [[succ M]] = λρ. let m be [[M]]ρ in m + 1 0 m = 0 [[pred M]] = λρ. let m be [[M]]ρ in m 1 m > 0 [[M]]ρ (l = 0) [[ifzero L then M else N]] = λρ. let l be [[L]]ρ in [[N]]ρ (l 0) [[rec f (x : τ) : τ. M]] = λρ. fix(λh. λv. [[M]](ρ, h, v)) 3.1 add : nat nat nat [[add]] [N [N N ] ] [[add]] = λx. fix(h x)
h [N [[N N ] [N N ]]] x (y = 0) h = λx. λ f. λy. let z be f (y 1) in z + 1 (y > 0) add 5.7 n, m N [[add n m]] = [[n + m]] = n + m [[add n m]] = fix(h n)(m) = h n (fix(h n)) m fix(h n) h n h n (fix(h n)) m = n + m m m = 0 h n (fix(h n)) 0 = n m > 0 h n (fix(h n)) m = let z be fix(h n) (m 1) in z + 1 fix(h n) (m 1) = n + m 1 h n (fix(h n)) m = n + m 1 + 1 = n + m [[add n m]] = [[n + m]] = n + m 6 Adequacy adequacy PCF adequacy 6.1 M : τ M V [[M]] = [[V]] M V [[fun(x : nat). 0]] = [[fun(x : nat). pred 1]] = λx. 0 fun(x : nat). 0 fun(x : nat). pred 1 (= ) nat nat nat 6.1
6.2 M : nat n N M n [[M]] = n 6.2 M : nat n N [[M]] = n M n M : τ [[M]] V C τ M V nat V, W [[V]] = [[W]] V = W Γ M : τ M fun(x : τ). M N W M [W/x] V M N V M N M [W/x] Plotkin [6] adequacy relation 7 Adequacy τ R τ [[τ]] C τ (n, m) R nat n = m ( f, fun(x : τ). M) R τ τ (v, V) R τ. ( f (v), M[V/x]) T(R τ ) T(R τ ) [[τ]] {M M : τ } (x, M) T(R τ ) y [[τ]]. x = y = ( V. M V (y, V) R τ ) 6.3 τ M : τ 1. (, M) T(R τ ) 2. d 0 d 1 [[τ]] (d i, M) T(R τ ) ( i N d i, M) T(R τ ) 6.4 (Basic Lemma) x 1 : τ 1,, x n : τ n M : τ ( v i, M i ) T(R τ i ) (1 i n) ([[M]](v 1,, v n ), M[M 1 /x 1,, M n /x n ]) T(R τ ) x 1 : τ 1,, x n : τ n M : τ 6.5 M : nat n N [[M]] = n M n 6.6 (Adequacy) M : nat n N [[M]] = n M n Adequacy M : nat [[M]] = 7 adequacy relation PCF
7 Full Abstraction full abstraction M, N : τ τ nat M, N M, N M C[M] : nat M C[ ] N C[N] : nat C[M] n = C[N] n M C[ ] N C[M] M N C[ ] : nat M PCF N M N M N ( 5.1 ) M N M N N M adequacy 7.1 τ M, N : τ [[M]] [[N]] M N 7.2 τ M, N : τ [[M]] = [[N]] M N 7.1 7.2 τ [[τ]] M : τ [[M]] x x [[τ]] parallel or 7.3 por τ [[[[τ]] N ] [[[τ]] N ] [[τ]] N ] 0 f (x) = 0 0 g(x) = 0 por τ ( f, g, x) = 1 n, m > 0. f (x) = n g(x) = m, otherwise Por τ = λ f. λg. λx. por τ ( f, g, x) [[(τ nat) (τ nat) τ nat]] f (x) ( g(x)) g(x) ( f (x)) 0 0 f (x), g(x) 0 1 por f (x) g(x) 0 0 PCF PCF 7.4 τ PCF M : (τ nat) (τ nat) τ nat [[M]] = Por τ
7.2 M 1, M 2 : ((nat nat) (nat nat) nat nat) nat M 1 M 2 [[M 1 x]](por nat ) [[M 2 x]](por nat ) 7.1 fully abstract fully abstract fully abstract full abstraction PCF full abstraction PCF por PCF PCF full abstraction [6, 2] PCF por [9, 5, 7] por [4, 1] 1990 PCF fully abstract Milner PCF fully abstract fully abstract PCF full abstraction [8, 3] proof reading Mikhov Rossen [1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Inf. Comput., 163(2):409 470, 2000. [2] R. Cartwright, P.-L. Curien, and M. Felleisen. Fully abstract semantics for observably sequential languages. Inf. Comput., 111(2):297 401, 1994. [3] K. Honda and N. Yoshida. Game-theoretic analysis of call-by-value computation. Theor. Comput. Sci., 221(1-2):393 456, 1999. [4] J. Hyland and C.-H. Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285 408, 2000.
[5] P. O Hearn and J. Riecke. Kripke logical relations and PCF. Inf. Comput., 120(1):107 116, 1995. [6] G. Plotkin. LCF considered as a programming language. Theor. Comput. Sci., 5:223 257, 1977. [7] J. Riecke and A. Sandholm. A relational account of call-by-value sequentiality. Inf. Comput., 179(2):296 331, 2002. [8] K. Sieber. Relating full abstraction results for different programming languages. In FST and TC 10: Proceedings of the tenth conference on Foundations of software technology and theoretical computer science, pages 373 387, New York, NY, USA, 1990. Springer-Verlag. [9] K. Sieber. Reasoning about sequential functions via logical relations. In Proc. LMS Symposium on Applications of Categories in Computer Science, LMS Lecture Note Series 177, pages 258 269. Cambridge University Press, 1992.