For a few minutes in our first PRL seminar of the season I mentioned several efforts I had been involved in to a greater or lesser extent over the Summer:

 

1) Rick Aaron completed his thesis, and I recommended reading his introduction to Nuprl because of his outside perspective. He is a user who simply adopted Nuprl as a tool for prototyping a body of formal math and tactics, as explained in his thesis, principally in order to exploit the tactic mechanism. He has not yet web-mounted his thesis, but you can see a postscript version of the excerpted Nuprl intro.

 

He will rework this as a standalone document that does not refer to thesis-specific contents, and we'll add it to the Nuprl documentation on our web pages.

 

2) In order to provide Aaron with adequate software to produce an indexed and cross referenced appendix comprising some of his library, I enhanced the methods for doing this in Nuprl4. This took a while.

 

3) Eli Barzilay is conducting research which will lead to a practical and elegant reflection of Nuprl, which he will discuss later. In this effort he is consulting with me, Constable, and Alexey Nogin. There have been some very interesting (to me) difficulties in simultaneously satisfying various requirements of the design. Eli has adopted Alexey's suggestion that terms-modulo-alpha-conversion be the basis for reflection, one consequence being that the (meta)operation of constructing an instance of a binding operator can itself be taken naturally as a binding operator, thus maintaining greater structural similarity when quoting a complex term operator-by-operator. (This is in contradistinction to considering the operation of constructing an instance of a binding operator (NOT-molulo-alpha-conv) as a function taking the binding variables explicitly as arguments; in that scenario, the (meta)operator is not a binding operator, since it just takes syntactic components, rather than syntacic functions, as arguments.)

 

4) Content production. The gradually growing body of discrete math lessons (prototypes) has been updated on the web, and the errors caused by switching to microsoft web servers have been avoided. See www.cs.cornell.edu/home/sfa/Nuprl/eduprl/Xone_one_corr_intro.html.

 

There are also a few "model" proofs together with verbalizations adapted from Amanda Holland-Minkley's recent verbalization study.

After participating in her study, I felt some of the original formal proofs (which were taken from the standard library) could be greatly improved, so I took the opportunity to rework them into examples of my own standards for readable formal proofs.

 

5) More web stuff.

 I will be rebuilding the libraries pointed to from the Nuprl project on www.cs.cornell.edu/Info/Projects/NuPrl/Nuprl4.2/Libraries and using the same style as for the web presentation of the content mentioned in (4) above. This will work the microsoft problem. Also, each theorem, which is HTML browsable node-by-node, is also linked to a postscript listing of the whole proof. Sadly, we have not yet gotten control over nested indentation (efforts have failed), so we are still limited as to the complexity of expression that can be readably projected from Nuprl from browsing. An intended improvement will be to link tactic names to descriptions, rather as Amanda did for her translation studies.

 

When this is done, the content mentioned in (4) will be linked to from the Nuprl library page.

 

6) Accounting.

I have continued thinking about the accounting methods for supporting arguments to the effect that because a proof occurs in the Nuprl5 system it is valid if the primitive rules employed are valid and the inference engines are correct. The occasion for this was the preparation of a white paper for a proposal including support for the design of such accounting mechanisms for Nuprl5. (This white paper was written mostly by Kreitz and Constable.) I took mentioning this in seminar as an opportunity to remind participants of some of the issues.

 

One of the main aspects of the design I have been working on is reliance on tactic code which, in the static context of the library slice upon which it "depends", has a fixed meaning and determines a unique inference (refinement). This is as opposed to the current situation in which the tactic source code is essentially a trace of the fact that at some time in the past, with some library, with some now-unknown interpretation of the tactic names and now-unknown values for some reference variables in a no longer extant ML state, the inference was produced. Such tactic code means little and it is currently only by great user discipline that the values upon which an inference depends can be made reconstructable.

 

(Alexey, who spoke after I did in seminar, gave us a brief idea of the methods he and Jason have been considering for making tactic code in MetaPrl meaningful in this sense.)

 

7) Naturally, I have continued thinking about type theory in the ways I presented in last semester's CS786- Computational Type Theory seminar. I expect to write about it this semester. See www.cs.cornell.edu/home/sfa/786_sfa6.html and www.cs.cornell.edu/home/kreitz/Teaching/CS786/00index.html.

 

8) I continued work on my approach to Second-order rule matching, and the so-called "derived rules". I expect to have a prototype implemented for Nuprl4 soon. Last semester Alexey gave a report in seminar on his progress on his approach to the same topic in MetaPrl, and I expect to give one this semester. The development is in part intended as a technical contribution to a discussion in the Nuprl group as to what form rules should take, especially in order to be able justify a formal rule by a formal proof.