課程名稱︰程式語言理論與型態系統 (FLOLAC) 課程性質︰資管系 (所) 選修 課程教師︰穆信成 (與教學團隊的其他講師) 開課學院：管理學院 開課系所︰資管系 (所) 考試日期（年月日）︰2018 年 7 月 20 日 考試時限（分鐘）：9:10 ~ 12:10 (最後有延長時間到 12:30) 試題 : Part (A) - Functional Programming Final Examination, July. 2018 Important: note before you start the exam: * Algebraic proofs need not be carried out in gory details -- you may skip some steps that you think are trivial. Do label the important steps, however, especially the step(s) where you use induction, or be explicit where you use fold fusion. * You can use all Haskell functions in the standard prelude, mentioned in the lectures. * You lost 1 point for each syntactical mistakes (e.g. writing f g x when it should be f (g x), or the other way round), up to 5 points. 1. (25 points) Assume the following definitions: maximum [] = -∞ maximum (x:xs) = x↑maximum xs , minimum [] = ∞ minimum (x:xs) = x↓minimum xs . Prove the following property maximum (map (x-) xs) = x - minimum xs . (1) You may use all properties regarding arithmetics, in particular laws regard- ing addition, subtraction, and minimum, and some silly ones such as x - ∞ = -∞. 2. (25 points) The function allpairs returns all pairs of elements in a given list, in their order: allpairs::List a → List (a,a) allpairs[] = [] allpairs(x:xs) = map (λy → (x,y)) xs ++ allpairs xs . For example, allpairs [1,2,3,4] evaluates to [(1,2),(1,3),(1,4),(2,3),(2,4), (3,4)]. Furthermore, the function maxdiff computes the maximum difference of these pairs: maxdiff::List Int → Int maxdiff = maximum.map minus.allpairs , minus (x,y) = x - y . Apparently, maxdiff as defined uses a O(n^2) algorithm. Define: mdm xs = (maxdiff xs,???) Find out what ??? should be, and construct a linear-time implementation of mdm. You may need properties such as: map f (xs ++ ys) = map f xs ++ map f ys , (2) maximum (xs ++ ys) = maximum xs↑maximum ys , (3) plus property (1), and other essential properties such as map-fusion. 3. Recall that map and minimum are both folds (definitions omitted... find out by yourself!): map f = foldr ? ? minimum = foldr ? ? Another way to prove (1) is to show that both sides equal the same fold. (a) (12 points) Turn maximum.map (x-) into a single foldr, using the foldr- fusion theorem. (b) (12 points) Turn (x-).minimum into a single foldr, using the foldr- fusion theorem. If they turn out to be the same foldr, you have proved (1). 4. (26 points) Given xs::List Int, the function call pure i xs checks whether there exists an element x in the j-th position such that x = i + j: pure i [] = False pure i (x:xs) = if i == x then True else pure (1+i) xs . For example, if xs = [1,4,2,5], pure 0 xs = True because xs!!2 = 2 = 0 + 2. People might be more used to do the same task imperatively. If we define: imp::MonadState Int m => List Int → m Bool imp [] = return False imp (x:xs) = get >>= λi → if i == x then put (1+i+length xs) >> return True else put (1+i) >> imp xs , where (>>) is defined by m >> n = m >>= λ() → n, the same computation can be done by put i >> imp xs. (There is an awkward put (1+i+length xs) before return True. You might see why we need it later.) Show that put i >> imp xs = put (i+length xs) >> return (pure i xs) . You may need monad laws, laws regarding get and put, and the if rule we have used a lot: f (if p then x else y) = if p then f x else f y for terminating p. Part (B) - Logic: Exam 12th Formosan Summer School on Logic, Language, and Computation, 2018 1. (20%) Give two different derivations of |- A → A. 2. (20%) Derive A Ｖ (B Λ C) |- (A Ｖ B) Λ (A Ｖ C). 3. (20%) Derive A → -A, -A → A |- ⊥. 4. (20%) Derive ∀x. P x → Q |- (∃x. P x) → Q. (P and Q are predicate symbols of arities 1 and 0 respectively.) 5. (20%) Prove that for all Γ⊆PROP, φ∈PROP, and Ψ∈PROP, if Γ|=φ and Γ|=Ψ, then Γ|=φΛΨ. Part (C) - Lambda Calculus and Types: Exam 12th Formosan Summer School on Logic, Language, and Computation In the following questions, you do not need to write down every step. 1. (20pt) Write the set of free variables for each of the following terms. (a) (λx.x y x) (λy.x) (b) λy.(λx.x y x) (c) λxyz.(λx.z) (d) (λy.λx.y x) x 2. (25pt) Give two untyped λ-terms N and M such that N ≠ M (no α equivalent), N /→ M, M /→ N (cannot β reduction) but there exists some L with N → L and M → L (can β reduction). Explain why. 3. (20pt) Recall that True = λxy.x and False = λxy.y. Reduce the following term to its normal form using →β* (β reduction with or without any intermediate step). (λn.n (λb.λxy.b y x)(λxy.x)) c_100 4. (20pt) Derive the following typing judgement for any type τ in simply typed lambda calculus. |- λb.λxy.b y x : (τ→(τ→τ)) → (τ→(τ→τ)) 5. (15pt) In Haskell, Maybe a is a type with constructors Nothing::Maybe a and Just::a → Maybe a for any type a. Consider a function defined by maybe :: b → (a→b) → Maybe a → b maybe b f Nothing = b maybe b f (Just a) = f a In System F, we can encode Maybe σ for any type σ as Maybe σ := ∀t.t → (σ → t) → t and Nothing as Nothing := Λt.λ(x:t)(f:σ→t).x Define the corresponding λ-terms Just : σ → Maybe σ maybe: ∀t.t → (σ → t) → Maybe σ → t in System F such that maybe τ b f (Just a) → f a (β reduction) maybe τ b f Nothing → b (β reduction) Part (D) - Models of concurrent computation and session types: Exam Marks: Each question below is 20% of the overall mark for the exam. 1. What are the free names and free variables of the following processes? (a) Q = (μb) ( b(x).Q_1 | b_bar<c> | x(y).Q_2 ) (b) R = (μa) (!a(x).c_bar<y>) | a(x).R_1 | b(y).0 ) 2. Are these processes structually congruent? Write the justification: (a) (μa)Q | P | !(P|(μa)Q) and (μa)(P|Q)|(!((μa)(P|Q))) (b) (μa)(c_bar<a> | a(x).a_bar<a>) and (μa)(c_bar<a> | b(x).b_bar<b>) 3. Write the reduction step by step using the rules in the lecture notes (you can omit some steps, such as the structural congruence). (a) (μb)(a(x).x_bar<b>) | !(a_bar<b> | b(x).0) (b) a_bar<e> | a_bar<b> | a(x).(b_bar<x> | c_bar<x>) 4. Give the dual types: (a) μt.(?[string];![string];?[boolean];t) (b) &{inc:?[nat];![boolean];end, dec:![string];end} 5. Give the type derivation: __________________________________________________________________ Ø;Ø|- s(x).s(y).s_bar< x<y >.0 |> s:?[int];?[int];![boolean];end Note that we assume the expression x < y evaluates to boolean. ------------------------------------------------------------------------------ 圖片連結： Part(A) - 1st page: https://goo.gl/ouGv17 Part(A) - 2nd Page: https://goo.gl/1Sj3LB Part(B): https://goo.gl/pKbBr6 Part(C): https://goo.gl/s1Deod Part(D): https://goo.gl/nAJ8vK --

※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 111.83.213.167 ※ 文章網址: https://webptt.com/m.aspx?n=bbs/NTU-Exam/M.1533324166.A.86E.html ※ 編輯: alan23273850 (36.235.34.5), 08/04/2018 21:14:00