API tools faq
paste
Guest User

Untitled

a guest
Oct 31st, 2018
37
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 5.33 KB | None | 0 0
raw download clone embed print report
  1. Section main.
  2. (*this program compiles with COQ 8.7*)
  3. (*The goal of this text is to show two famous undecidability results, namely
  4. the Rice theorem and the Turing halting theorem on a simplistic yet -hopefully- convincing
  5. computation model. We make 4 assumptions listed below (and in the case of the halting
  6. problem, we add the further assumption that there exists at least one non terminating
  7. program, since in the opposite case the constant function which returns true would be
  8. a perfectly reliable halting test*)
  9.  
  10. Variables Input Output:Type.
  11. Variable pairing: Input -> Input -> Input. (*We assume we have a syntactic operation
  12. which makes an input with two other inputs, like putting parentheses*)
  13. Variable Calculate: Input -> Output -> Prop. (*We have an interpreter and
  14. "Calculate a b" means that when a is submitted to the interpreter, we get b as a result*)
  15. Variable b_false b_true:Output. (*booleans*)
  16.  
  17. (*we introduce convenient notations*)
  18. Notation "a [ b ]" :=(pairing a b) (at level 61).
  19. Notation "p >>> q" := (Calculate p q) (at level 71).
  20. Notation same_result:= (fun a b:Input => forall r:Output, a >>> r <-> b >>> r).
  21. Notation halts := (fun x:Input => exists r:Output, x >>> r).
  22.  
  23. Hypothesis A1: b_true <> b_false. (*the booleans are different*)
  24.  
  25. Hypothesis A2: forall (x:Input) (a b:Output),
  26. x >>> a ->
  27. x >>> b ->
  28. a = b. (*if the result of a computation exists then it is unique*)
  29.  
  30. Hypothesis A3: forall x:Input, exists diag_x:Input,
  31. forall (y:Input),
  32. same_result (diag_x [y]) (x [y[y]]). (*it is possible to handle parenthesis
  33. in the system in order to do this*)
  34.  
  35. Hypothesis A4: forall condition case_1 case_2:Input, exists if_loop:Input, forall x:Input,
  36. (condition [x] >>> b_true -> same_result (if_loop [x]) case_1) /\
  37. (condition [x] >>> b_false -> same_result (if_loop [x]) case_2).
  38. (*our system handles if-then-else*)
  39.  
  40. Theorem fixed_point: forall x:Input, exists e:Input,
  41. same_result e (x[e]).
  42. Proof.
  43. intro.
  44. destruct A3 with (x:=x) as (dx, D).
  45. exists (dx [dx]).
  46. apply D.
  47. Qed.
  48.  
  49. Section no_semantical_tests.
  50.  
  51. (*the Rice theorem states the three conditions below cannot hold simultaneously, namely
  52. there is no boolean non constant test which depends only on what a program actually does,
  53. and which can be programmed in the system we're discussing*)
  54.  
  55. Variables test x1 x2: Input.
  56.  
  57. Hypothesis T1:forall x y:Input, same_result x y -> same_result (test[x]) (test[y]).
  58. Hypothesis T2: forall x:Input, test[x] >>> b_true \/ test[x] >>> b_false.
  59. Hypothesis T3: test[x1] >>> b_true /\ test[x2] >>> b_false.
  60.  
  61. Theorem Rice: False.
  62. Proof.
  63. destruct A4 with (condition:= test) (case_1 := x2) (case_2 := x1) as (u,Hyp_u).
  64. destruct fixed_point with (x:=u) as (e, Fix_ue).
  65. apply A1.
  66. destruct T2 with (x:=e).
  67. apply A2 with (x:= test [e]).
  68. assumption.
  69. apply T1 with (x:= x2).
  70. intro.
  71. apply iff_sym.
  72. apply iff_trans with (B:= u [e] >>> r).
  73. apply Fix_ue.
  74. apply Hyp_u.
  75. assumption.
  76. apply T3.
  77. apply A2 with (x:= test [e]).
  78. apply T1 with (x:= x1).
  79. intro.
  80. apply iff_sym.
  81. apply iff_trans with (B:= u [e] >>> r).
  82. apply Fix_ue.
  83. apply Hyp_u.
  84. assumption.
  85. apply T3.
  86. assumption.
  87. Qed.
  88.  
  89. End no_semantical_tests.
  90.  
  91. Section halting_problem.
  92.  
  93. Variable halting_test: Input.
  94.  
  95. Hypothesis HT1: exists stall:Input, halts stall -> False.
  96. Hypothesis HT2: forall x:Input, halting_test [x] >>> b_true <-> halts x.
  97. Hypothesis HT3: forall x:Input,
  98. halting_test [x] >>> b_true \/ halting_test [x] >>> b_false.
  99.  
  100. Lemma calc_equality: forall (p q:Input) (r:Output),
  101. p >>> r -> q >>> r -> same_result p q.
  102. Proof.
  103. intros.
  104. intro.
  105. split.
  106. intro.
  107. assert (r = r0).
  108. apply A2 with (x:=p).
  109. assumption.
  110. assumption.
  111. rewrite <- H2.
  112. assumption.
  113. intro.
  114. assert (r = r0).
  115. apply A2 with (x:=q).
  116. assumption.
  117. assumption.
  118. rewrite <- H2.
  119. assumption.
  120. Qed.
  121.  
  122.  
  123. Theorem Turing_halting_theorem: False.
  124. Proof.
  125. destruct HT1 as (stall,Hyp_stall).
  126. apply Rice with (test:=halting_test) (x1 := halting_test [stall]) (x2:= stall).
  127. intros.
  128. destruct HT3 with (x:=x).
  129. apply calc_equality with (r:= b_true).
  130. assumption.
  131. apply HT2.
  132. apply HT2 in H0.
  133. destruct H0 as (rx, X).
  134. exists rx.
  135. apply H.
  136. assumption.
  137. apply calc_equality with (r:= b_false).
  138. assumption.
  139. destruct HT3 with (x:=y).
  140. apply False_ind.
  141. apply A1.
  142. apply A2 with (x:= halting_test [x]).
  143. apply HT2 in H1.
  144. destruct H1 as (ry, Y).
  145. apply HT2.
  146. exists ry.
  147. apply H.
  148. assumption.
  149. assumption.
  150. assumption.
  151. apply HT3.
  152. split.
  153. apply HT2.
  154. destruct HT3 with (x:=stall).
  155. exists b_true.
  156. assumption.
  157. exists b_false.
  158. assumption.
  159. destruct HT3 with (x:=stall).
  160. apply False_ind.
  161. apply Hyp_stall.
  162. apply HT2.
  163. assumption.
  164. assumption.
  165. Qed.
  166.  
  167. End halting_problem.
  168.  
  169. End main.
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!