theory s1 imports Main begin section "Q1: \-Calculus" (* TODO: provide your answers here or in an separate PDF file *) text \ Q1 (a) \ term "(x y)(\x.(\y.(\z.(z(x y)))))" term "x y (\x.(\y.(\z.(z(x y)))))" (* application binds to the left *) term "x y (\x.\y.\z. z(x y))" (* abstraction binds to the right *) term "x y (\x y z. z(x y))" (* list variables for \ *) text \ Q1 (b) \ (* term given in the question *) (*term "x (\x y. x (y z) (x y)) (\y. y z)"*) (* with parentheses restored *) (*term "(x (\x. (\y. ((x (y z)) (x y))))) (\y. (y z))"*) text \ Q1 (c) \ text \ (\f.\x.f(f(fx)))(\g.\y.g(gy)) ----------------------------- \ \x.(\g.\y.g(gy))((\g.\y.g(gy))((\g.\y.g(gy))x)) -------------- \ \x.(\g.\y.g(gy))((\g.\y.g(gy))(\y.x(xy))) alpha (not necessary) \ \x.(\g.\y.g(gy))((\g.\z.g(gz))(\y.x(xy))) ----------------------- \ \x.(\g.\y.g(gy))(\z.(\y.x(xy))((\y.x(xy))z)) ----------- \ \x.(\g.\y.g(gy))(\z.(\y.x(xy))(x(xz))) ----------------- \ \x.(\g.\y.g(gy))(\z.x(x(x(xz)))) ----------------------------- \ \x.(\y.(\z.x(x(x(xz))))((\z.x(x(x(xz))))y)) ----------------- \ \x.(\y.(\z.x(x(x(xz))))(x(x(x(xy))))) ----------------------------- \ \x.(\y.x(x(x(x(x(x(x(xy)))))))) \ text \ Q1 (d) \ text \ exp = \m n. n m For the justification, show that exp (\f.\x.f^n x) (\f.\x.f^m x) beta-reduces to \f.\x.f^(m^n) x using the previous question and reasonable omissions. Here, f^n x abbreviates f(f(...(f x))) (n-fold application of f to n). (\f.\x.f^n x) (\f.\x.f^m x) \ \y.(\f.\x.f^m x)^n y (beta+alpha) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...((\f.\x.f^m x)((\f.\x.f^m x) y))) (n-times repeat) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.(\x. y^m x)^m x)) (beta, n-1) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.(\x. y^m x)...((\x. y^m x)((\x. y^m x) x))))) (n-1, m) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.(\x. y^m x)...((\x. y^m x)(y^m x))))) (beta, n-1, m-1) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.(\x. y^m x)...(y^m (y^m x)))))) (beta, n-1, m-2) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.(\x. y^m x)...(y^(m+m) x)))) (n-1, m-2) \ \y.(\f.\x.f^m x)((\f.\x.f^m x)...(\x.y^(m^2) x)) (beta*,n-2) \ \y.(\f.\x.f^m x)(\x.y^(m^(n-1)) x) (beta*) \ \y.(\x.(\x.y^(m^(n-1)) x)^m x) (beta) \ \y.(\x.y^(m^n) x) (beta*) \ section "Q2: Types" (* TODO: provide your answers here or in an separate PDF file *) text \ Q2 (a) \ context notes [[show_types]] begin term "\ a b. a (c b) b" end text \ \lambda a b. a (c b) b has type ('a => 'b => 'c) => 'b => 'c in the context that gives c: 'b => 'a \ text \ Type derivation: Let \ \ [a::'a => 'b => 'c, b::'b, c::'b => 'a] and \' \ [a::'a => 'b => 'c, c::'b => 'a]. ------------ Var ----------- Var \ \ c::'b=>'a \ \ b :: 'b ----------------- Var --------------------------------- App \ \ a::'a=>'b=>'c \ \ cb::'a -------------------------------------------- App ---------- Var \ \ a(cb)::'b=>'c \ \ b::'b -------------------------------------------------------------- App \ \ a(cb)b::'c ------------------------ Abs \' \ \b.a(cb)b::'b=>'c --------------------------------------------- Abs c::'b=>'a \ \ab.a(cb)b::('a=>'b=>'c)=>'b=>'c \ text \ Q2 (b) \ context notes [[show_types]] begin term "\ x y z. z y (x y)" end typ "('a \ 'b) \ 'a \ ('a \ 'b \ 'c) \ 'c" text \ 2 (c) \ text \Argue that, if the term is typable, the type should be derived by applying the typing rules given in the lecture. However, there is no rule that can be applied to xx because x cannot have the type of the function and the argument at the same type in the Application rule.\ text \ 2 (d) \ text \ (\xy.y)(\z.zz) \ \y.y :: 'a => 'a \ text \ 2 (e) \ text \The term is not typable, which follows from Q2(c). The subject reduction says that the type of a term does not change after applying beta-reductions. The situation here is that a term that is not typable may become typable after some beta-reduction, indicating that the typable property is preserved only in the direction of the reduction but not backwards.\ text \ Question 3 \ lemma prop_a: "A \ \\A" apply (rule impI) apply (rule notI) apply (erule notE) apply assumption done lemma prop_b: "\\\ A \ \A" apply (rule impI) apply (rule notI) apply (erule notE) apply (rule notI) apply (erule notE) apply assumption done lemma prop_c: "\\ A \ A" apply (rule impI) apply (case_tac A) apply assumption apply (erule notE) apply assumption done (* lemma prop_d: "(\A \ False) \ A" apply (rule impI) apply (case_tac A) apply assumption apply (drule mp) apply assumption apply (erule notE) apply (erule FalseE) done *) lemma prop_d: "\(A \ B) \ \ A \ \ B" apply (rule impI) apply (case_tac A) apply (rule disjI2) apply (rule notI) apply (erule notE) apply (rule conjI) apply assumption+ apply (rule disjI1) apply assumption done lemma prop_e: "(A \ B) \ (\ A \ B)" apply (rule impI) apply (case_tac A) apply (drule mp) apply assumption apply (rule disjI2) apply assumption apply (rule disjI1) apply assumption done lemma prop_f: "\A\\B \ \(A\B)" apply (rule iffI) apply (rule notI) apply (erule disjE) apply (erule conjE) apply (erule notE) apply assumption apply (erule conjE) apply (erule_tac P=B in notE) apply assumption apply (rule conjI) apply (rule notI) apply (erule notE) apply (rule disjI1) apply assumption apply (rule notI) apply (erule notE) apply (rule disjI2) apply assumption done lemma prop_g: "(A \ B) \ (((B \ C) \ A) \ B)" apply (rule impI) apply (rule impI) apply (case_tac B) apply assumption apply (erule impE) apply (erule impE) apply (rule impI) apply (erule notE) apply assumption+ done text \ Question 4 \ lemma hol_a: "(\x. P x \ Q) \ (\x. P x) \ Q" apply (rule impI) apply (rule impI) apply (erule exE) apply (erule mp) apply (erule_tac x=x in allE) apply assumption done lemma hol_b: "((\x. P x) \ Q) \ (\x. P x \ Q)" apply (rule iffI) apply (rule allI) apply (rule impI) apply (erule mp) apply (rule_tac x=x in exI) apply assumption apply (rule impI) apply (erule exE) apply (drule_tac x=x in spec) apply (erule mp) apply assumption done lemma hol_c: "(\x. P x) \ \ (\x. \ P x)" apply (rule iffI) apply (rule notI) apply (erule exE) apply (drule_tac x=x in spec) apply (erule notE) apply assumption apply (rule allI) apply (rule classical) apply (erule notE) apply (rule_tac x=x in exI) apply assumption done lemma hol_d: "(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)" apply (rule impI) apply (rule conjI) apply (rule allI) apply (drule_tac x=x in spec) apply (erule conjE) apply assumption apply (rule allI) apply (drule_tac x=x in spec) apply (erule conjE) apply assumption done lemma hol_e: "(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)" apply (rule impI) apply (erule exE) apply (erule disjE) apply (rule disjI1) apply (rule_tac x=x in exI) apply assumption apply (rule disjI2) apply (rule_tac x=x in exI) apply assumption done lemma hol_f: "(\x y. A y \ B x) \ (\x. B x) \ (\y. A y)" apply (rule impI) apply (case_tac "(\x. A x)") apply (rule disjI2) apply assumption apply (rule disjI1) apply (rule allI) apply (rule ccontr) apply (drule_tac x=x in spec) apply (erule notE) apply (rule allI) apply (drule_tac x=xa in spec) apply (erule disjE) apply assumption apply (erule notE) apply assumption done end