69 lines
1.7 KiB
OCaml
69 lines
1.7 KiB
OCaml
(*
|
|
https://ocaml.org/learn/tutorials/up_and_running.html
|
|
|
|
[dune init exe proof_false]
|
|
|
|
made this
|
|
|
|
[let () = print_endline "Hello, World!"]
|
|
*)
|
|
|
|
let rec inf arg = inf arg
|
|
(*
|
|
# let rec inf arg = inf arg;;
|
|
val inf : 'a -> 'b = <fun>
|
|
*)
|
|
|
|
(* Let's say that [void] represents the False type *)
|
|
type void = {nope : 'a . 'a}
|
|
|
|
|
|
(*
|
|
Warning! Eager evaluation for function args.
|
|
ie, the following line is an infinite loop
|
|
and wouldn't finish.
|
|
*)
|
|
let ff : void = inf ()
|
|
|
|
(*
|
|
Here, [ff] is a value of False type ([void]).
|
|
ie, [ff] is a proof of False.
|
|
That means that we just gave a proof for False,
|
|
which is absurd.
|
|
|
|
It's okay in OCaml as it's not intended to make proofs, unlike Coq.
|
|
Coq would never allow this.
|
|
|
|
To avoid proofs of False type, we need to avoid infinite loops. But we have a
|
|
problem there.
|
|
Because that would mean that the coq compiler would need to figure out which
|
|
programs would terminate and which won't.
|
|
|
|
And that's the famous Halting problem, which states that no program can
|
|
accurately say if another program would terminate (ie, halt) or not.
|
|
|
|
ie, Halting problem is an undecidable problem.
|
|
|
|
Therefore, it's impossible for coq compiler to accurately weed out non-terminating
|
|
programs.
|
|
So it does the next best thing. It disallows recursions which aren't structurally
|
|
decreasing.
|
|
Unfortunately this also means that some valid programs would also be rejected.
|
|
|
|
Every function call is made upon a 'smaller' form of an argument.
|
|
And eventually the argument we will reach a base case where the argument is
|
|
small enough that no more recursion would be possbile (as the arg can no longer
|
|
be made 'smaller').
|
|
|
|
`{struct}`
|
|
|
|
|
|
*)
|
|
|
|
(*
|
|
[dune build]
|
|
[dune exec ./proof_false.exec]
|
|
|
|
The .exe is needed in linux as well.
|
|
*)
|