Mark, I think you can write some good Light documentation, and maybe improve
the HOL Light code. Let me try to explain. My only objection to my
PrintErrorFail is minor: it prints
Exception: Failure "".
at the end, but arguably this is a good error message. Here's what I like
about my def:
1) I took it my def
let PrintErrorFail s =
open_box 0; print_string s; close_box (); print_newline (); fail();;
from the first half of a sentence at the top of the Ocaml reference manual
section
21.9 Module Format : Pretty printing:
For instance, the sequence open_box 0; print_string "x ="; print_space ();
print_int
1; close_box (); print_newline () that prints x = 1 within a pretty-printing
box, can be
abbreviated as printf "@[%s@ %i@]@." "x =" 1, or even shorter printf "@[x =@
%i@]@." 1.
2) "fail" has an link in the HOL Light reference manual, and "failwith" is only
explain in the "fail" link:
In general, the failure can be generated by failwith "string", but
the special case of an empty string is bound to the function fail.
I think that you understood a great deal more about pretty-printing error
messages, and I advise you to try to write up what you know. We need good
documentation. Perhaps you understand printer.ml well enough to recommend some
change by which all HOL Light error messages are pretty-printed. I certainly
don't see how to do this.
But I'm not happy with is my understanding of the Toploop/Obj.magic/Lexing code
I borrowed from Freek's miz3.ml. I hope you can write some good documentation
here as well. I just looked at your Tactician sources, and I have some
non-expert responses:
This from mlconcrete.ml
(* ** GRABBING INFORMATION FROM THE OCAML ENVIRONMENT ** *)
(* This is closely based on Zumkeller's mechanism for automatically updating *)
(* the HOL Light theorem database. *)
(* Execution of any OCaml expression given as a string *)
(* Execution of any OCaml expression given as a string *)
let exec x =
(ignore o Toploop.execute_phrase false Format.std_formatter o
!Toploop.parse_toplevel_phrase o Lexing.from_string) x;;
looks pretty similar to the code I borrowed from miz3.ml. Can you explain it?
Is this different from the Roland Zumkeller's Flyspeck code you mention in
autopromote.ml? Is this explained in Flyspeck somewhere? I see that in
termparser.ml you have
let enable_flyspeck_parsing () =
let env = Obj.magic !Toploop.toplevel_env in
I bet it would be a really good programming exercise for me to really
understand how Toploop/Obj.magic/Lexing code is used in the Ocaml sources, or
Flyspeck, or your Tactician. But I'd rather you explain it to me so I can read
Voevodsky's book http://homotopytypetheory.org/2013/06/20/the-hott-book/.
I've made a little progress:
A homotopy theorist I know said it's easy to understand as homotopy theory.
That encouraged me, and I see he has his own section in the book:
9.9 The Rezk completion . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 316
I don't see that yet, but I did see, on p 8,
On the other hand, this notion of “or” is so strong that a naive
translation of the law of excluded middle is inconsistent with the
univalence axiom.
I knew Coq was about constructivity, but I didn't know that Voevodsky's big
axiom was so constructive. And they explain it:
For if we assume “for all A, either A or not A”, then since proving
“A” means exhibiting an element of it, we would have a uniform way
of selecting an element from every nonempty type — a sort of
Hilbertian choice operator. However, univalence implies that the
element of A selected by such a choice operator must be invariant
under all self-equivalences of A, since these are identified with
self-identities and every operation must respect identity. But
clearly some types have automorphisms with no fixed points, e.g. we
can swap the elements of a two-element type.
That makes sense, but I like the HOL Light Hilbert choice operator @. The book
continues:
Fortunately, homotopy type theory gives a finer analysis of this
situation, allowing various different kinds of logic to coexist and
intermix.
Good!
The new insight that makes this possible is that the system of all
types, just like spaces in classical homotopy theory, is
“stratified” according to the dimensions in which their higher
homotopy structure exists or collapses. In particular, Voevodsky
has found a purely type-theoretic definition of homotopy n-types,
corresponding to spaces with no nontrivial homotopy information
above dimension n. (The 0-types are the “sets” mentioned previously
as satisfying Lawvere’s axioms.) Moreover, with higher inductive
types, we can universally “truncate” a type into an n-type; in
classical homotopy theory this would be its nth Postnikov section.
I think I understand this. We can build a topological space out of its
homotopy groups, and the nth Postnikov space is built out of the first n
homotopy groups. So the bigger n is, the more information we have. I'd guess
that if n = -1, we're missing a lot of information.
Most of classical mathematics which depends on the law of excluded
middle and the axiom of choice can be performed in univalent
foundations, simply by assuming that these two principles hold (in
their proper, (−1)-truncated, form).
So if we need the law of excluded middle and the axiom of choice, we're only
seeing a small sliver of Voevodsky's homotopy theory?
--
Best,
Bill
------------------------------------------------------------------------------
Get your SQL database under version control now!
Version control is standard for application code, but databases havent
caught up. So what steps can you take to put your SQL databases under
version control? Why should you start doing it? Read more to find out.
http://pubads.g.doubleclick.net/gampad/clk?id=49501711&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
