HomePage RecentChanges

Bourbaki questions

I am impressed! This is some beautiful work! And verify.lisp is amazingly short. Wow. I haven't tested it yet, nor fully digested the documentation, but wow. Nice!

A few questions?

1. "The relative order of independent proof lines does not matter."

I'm not clear on why that is. Or what "independent proof lines" means.

If neither line depends on the other for any hypotheses, the order is free (and one line can be used to satisfy hypotheses for multiple lines further down) – jarpiain

2. My editor can read/write UTF-8 but can only handle certain codesets, and only one at a time! Doh. Apparently bourbaki accepts any UTF-8 character as the name of a symbol, then I need a text editor that can mix and match codesets. What tool are you using?

almost certainly the answer would be "emacs"; since "where there is lisp, there shall ye find the editor" (Prolambdas) --jcorneli
actually "gvim" with a hacked keyboard layout. Maybe I should upload an ASCII version of prop.lisp at least – jarpiain

3. On symtrees: "The tree is well-formed if the number of arguments of op is n and each treei is a well-formed tree whose type is a subtype of the corresponding argument type of op."

Beautiful! That solves the problem of "overloaded" functions very nicely!

Question: does bourbaki check for loops in the super/sub-type declarations? Or is that the user's responsibility?

Not checked currently (nor are vicious circles in proofs: the verifier goes to an infinite loop instead of printing a clean error message). Probably at some future version, but not worth the effort now – jarpiain

4. Symbol arguments: are null substitutions allowed? For example, in Metamath a given type could be specified as permitting nulls with an axiom of this sort:

    nullXYZ $a xyz $.
Null symtrees are explicitly not allowed by proper-wff-p. (For no particular reason. Is there any use for them? A null symtree would fail any type check) – jarpiain
Just asking. I hate nulls :) --ocat

5. Doc clarification --

In your definitions "lisp-form*" is used but not defined. I'm assuming that is common knowledge to Lisp programmers, but ??? For example in 4.1.1:

    theorem-form := ( th name var-spec lisp-form* )
Anything that can be evaluated by Common Lisp. Again, some future version will probably include sandboxing to prevent the user from calling delete-file, say. – jarpiain

6. How much for a software license?

First born? Oath of fealty? Or is it GPL?

Definitely GPL if you look in the tarball & at the top of the source files. --jcorneli

--ocat 20-Oct-2005

7. I am wondering, jarpiain, if you have/would consider the Ghilbert approach of separating proofs from theorems. Essentially, a theorem can be considered as an assertion without a proof, like an axiom. Bourbaki has so much in common with Ghilbert I wonder if we could strive for unification at the conceptual level, assuming that the change(s) add to Bourbaki in an elegant and useful way. --ocat

Hmm, I need to re-read the ghilbert design doc. Maybe an interface file for a Bourbaki context could be autogenerated by writing the theorems with class changed to 'axiom', and omitting the proofs. Then a reference to the context (e.g. !!logic) would first try to load the interface file. --jarpiain

8. Are there any places other than symbol name that would need to be addressed if a user desired to create a 7-bit ASCII version of Bourbaki? (It has been noted that typesetting will be desireable anyway, so the utility of Unicode seems less than its drawbacks for some users…) --ocat

The code is actually encoding-agnostic. Use whatever encoding you want for the symbols, but make sure the Lisp reader understands it. And of course ASCII is a subset of UTF-8. --jarpiain