87 views

Skip to first unread message

Jan 18, 2016, 6:59:33 PM1/18/16

to metamath

On Mon, Jan 18, 2016 at 2:49 PM, Norman Megill <n...@alum.mit.edu> wrote:

(in an earlier post you wrote:)

>In fact, it may be necessary to wait for this before reorganizing, >because unless you have a tool for fixing all the proofs after such a >change I'm not sure how it can be done.

Suppose we want to change the order of hypotheses for theorem xyz. The way I do it now is to make a copy of it then rename the original and its references to xyzOLD. The copy becomes the new xyz after getting its proof to work locally (hypotheses can be swapped safely if the proof is saved as /normal). Then we go into MM-PA for each proof using xyzOLD and do 'minimize_with xyz/allow_growth' to replace each reference to xyzOLD with xyz.

That actually wouldn't work in this case, because a change to $f order causes all theorems to have their hypotheses reordered, and there is no way to specify a different order. For example, if we have

$v x y $.

vx $f set x $.

vy $f set y $.

weq $a wff x = y $.

vx $f set x $.

vy $f set y $.

weq $a wff x = y $.

then weq will have the hypothesis order [vx, vy]. If we try to make a copy of it -

weqOLD $a wff x = y $.

this will also have hypothesis order [vx, vy]. Changing the order of vx and vy will cause both axioms to have their hypothesis list reordered, you can't have both in the same database (except, ironically, if you use local variables). Alternatively, you could use

weqOLD $a wff y = x $.

weqOLD $a wff y = x $.

which would have the desired effect, but such a redefinition requires a lot more "creativity" in selecting variable names that have the desired relative orders, and would not be much better than /explicit.

I suppose it's (far) too late to change this, but I would have preferred that $f hyps come in the order they show up in the expression itself, that is, something like wbr $a wff A R B $. should have its arguments come in the order [cA, cR, cB]. If there are $e hyps then it would be the order that variables show up in text order, i.e. for

eqtrd.1 $e |- ( ph -> A = B ) $.

eqtrd.1 $e |- ( ph -> A = B ) $.

eqtrd.2 $e |- ( ph -> B = C ) $.

eqtrd $p |- ( ph -> A = C ) $.

we would have arguments [wph, cA, cB, cC]. There is of course the present advantage that $f hyps can be freely reordered, and a $a or $p will not change its order unless its math string changes. It also means that a grammar parse comes in basically infix notation, meaning that an expression ( 1 * ( 2 ( f ` 3 ) 4 ) ) has leaf nodes in the order [1, *, 2, f, 3, 4], which you would expect, rather than the current non-obvious order [1, 2, 4, 3, f, *]

This should be fine, as it doesn't affect the theoretical results above.

OK, in order to simplify writing parsers, we can add to the spec that redeclaration of a variable type ($f) must match any previous $f for that variable. No database violates this now AFAIK, and if does it can be easily fixed.

As for Appendix C, it assumes that the database has been pre-processed into abstract "frames" (p. 164 bottom) where each variable used in the frame is assigned a unique type ($f). Since each statement's frame is self-contained, I don't think it matters if a variable is assigned a different type in some other frame. It is possible that I am overlooking something.

This is true.
But it leaves a "variable" ($v) in a strange position, since it really
isn't meaningful without an $f to go with it. This passes directly to
the theoretical framework of Appendix C; I once tried to define the
subset of EX_C that represents provable formulas, but I can't without an
assignment of all the variables to typecodes, i.e. a frame, which makes
it sound like a local property when it's not. Here is an alternative definition of appendix C with a global type function.

> Let CN be a set, the set
of constants, and VR be another set disjoint from CN, denoting the
variables. Let Type be a function from VR to CN, this maps a variable to
its typecode. Then define SM = CN u. VR, EX = U_ n e. om SM^n, EX_C = {
e e. EX | |e| > 0 /\ e_0 e. CN }, DV = { x C_ VR | |x| = 2 }, VT = { <Type(v), v> | v e. VR }. The function V(E), where E e. EX, is V(E) = VR i^i ran E, and V(S) for S C_ EX is V(S) = U_ e e. S V(e).

> A substitution is a function σ : EX -> EX such that σ(<c>) = <c> for c e. CN and σ(a concat b) = σ(a) concat σ(b).

>
A pre-statement is a tuple <D, H, A> with D C_ DV, H C_ EX_C is
finite, and A e. EX_C. The reduct of <D, H, A> is <D_M, H,
A> where D_M = { x e. D | x C_ V(H u. {A}) }, and a statement is the
reduct of some pre-statement.

> A formal system is a tuple <CN, VR, Type, Γ> where Γ is a set of statements. The closure of a set H C_ EX_C relative to D is the smallest set C such that H u. VT C_ C, and for every <D', H', A'> e. Γ and every substitution σ, if A. h e. (H' u. VT) σ(h) e. C and A. {a,b} e. D' A. c e. V(σ(<a>)) A. d e. V(σ(<b>)) {c,d} e. D, then σ(A') e. C. A pre-statement <D, H, A> is
provable if A is in the closure of H relative to D, and a statement is
provable if it is the reduct of a provable pre-statement. The universe
of a formal system is its set of provable statements.

I
reiterated most of the definitions unchanged, so that it is clear what
is and is not changed. The difference is Type, which is now a global
function on VR, and VT replaces the local variable T in pre-statements.
In particular, we can make the following definition:

> The distinct universe of a formal system is the closure of the empty set relative to DV.

This is the set of expressions derivable in a theorem with no hypotheses where all variables are assumed distinct.

I'll show a bit more work I've done on the model theory of metamath, which is now easier to state with a global type function.

>
Let TC be the set { A_0 | <D, H, A> is provable }. This is the
set of typecodes (in set.mm, this would be {set, class, wff, |-}). Fix a
function OV on TC, which represents the universe for each typecode. (In
set.mm, OV(class) is roughly the ZFC universe, OV(wff) is {0,1}, OV(|-)
is {1}, and OV(set) is {v0, v1, ...}.) Let OM be the set of object
morphisms, that is functions τ on VR such that τ(v) e. OV(Type(v)) for
all v e. VR. (This can be thought of as a variable assignment, but to
objects of the universe, not expressions.)

> A model of a formal system is a tuple <OV, Δ, η> where Δ is a symmetric relation on the disjoint union of OV(c), and η_τ is a OM-indexed family of partial function on EX_C such that for all τ e. OM:

> * for all e e. EX_C, if η_τ(e) is defined then η_τ(e) e. OV(Type(e_0)),

> * η_τ(<Type(v), v>) = τ(v) for v e. VR, and

> A model of a formal system is a tuple <OV, Δ, η> where Δ is a symmetric relation on the disjoint union of OV(c), and η_τ is a OM-indexed family of partial function on EX_C such that for all τ e. OM:

> * for all e e. EX_C, if η_τ(e) is defined then η_τ(e) e. OV(Type(e_0)),

> * η_τ(<Type(v), v>) = τ(v) for v e. VR, and

> * For each <D, H, A> e. Γ, if τ(a) Δ τ(b) for all {a,b} e. D and η_τ(h) is defined for all h e. H, then η_τ(A) is defined.

> Additionally, the η_τ functions are connected by the substitution principle: For any substitution σ, η_τ(σ(e)) = η_σ(τ)(e), where σ(τ) is defined such that σ(τ)(v) = η_τ(σ(<Type(v), v>)).

Just
a little teaser, I hope to get a paper out of the above. As an example
for prop calc, we have OV = {wff -> {0, 1}, |- -> {1}} (the universe of wffs is
two elements), Δ = (/) (doesn't matter, since wff $d's don't occur), and η_τ is the smallest function such that η_τ("wff v") = τ(v) for each wff variable v, and η_τ("wff -. ph") = 1 - η_τ("wff ph") and η_τ("wff ( ph /\ ps )") = η_τ("wff ph") * η_τ("wff ps") for any wff strings ph, ps. Additionally, η_τ("|- v") = 1 if η_τ("wff v") = 1, otherwise it is undefined.

As for otherwise allowing local scopes for $v and $f, I assume you find that ok? Although it isn't needed now, I'm anticipating a hypothetical case with hundreds of dummy variables whose overhead we don't want to affect the remainder of set.mm.

Mario

Jan 19, 2016, 6:32:05 PM1/19/16

to meta...@googlegroups.com

affecting one theorem, not $f's that affect many theorems. One way to

do it is as follows.

Suppose we want to move 'vq $f set q' somewhere else. Rename vq, q to

vqOLD, qOLD (throughout set.mm) then insert

$v q $.

vq $f set q $.

where you want the vq to move to.

Suppose abc is the first theorem referencing vqOLD. Make a copy of

theorem abc and rename the original to abcOLD. Save the proof of the

new abc in /normal format then change qOLD to q and vqLD to vq. Then

change all references to abcOLD to abc by using

'minimize.../allow_growth' as I described before.

Repeat this all the way down until no more theorems reference vqOLD.

Of course, this is a too large a task to do by hand, and it would have

to be automated with a somewhat complex script.

Maybe waiting for the /explicit proof format is the practical thing to

do. I'll move it up on my to-do list.

Norm

Jan 29, 2016, 2:04:17 AM1/29/16

to meta...@googlegroups.com

On 1/19/16 6:32 PM, Norman Megill wrote:

> Maybe waiting for the /explicit proof format is the practical thing to

> do. I'll move it up on my to-do list.

>

> Norm

Version 0.123 of the metamath program adds a new /explicit proof format
> Maybe waiting for the /explicit proof format is the practical thing to

> do. I'll move it up on my to-do list.

>

> Norm

that allows hypotheses ($e, $f) in set.mm to be reordered without any

side effects. It is available here:

http://us2.metamath.org:88/index.html#mmprog

Specifically, the following features were added to metamath.exe:

1. The /packed qualifier is now available for 'show [new_]proof' and

'save [new_]proof'. (Originally it was available, but undocumented, for

'save'.)

2. A new /explicit qualifier is available with /normal and /packed

formats in 'show' and 'save' proofs.

The current /normal proof is a list of labels. The /packed format is an

extension to /normal that adds local labels "<nn>:" to subproofs that

can be referenced later in the proof without repeating them. The

/explicit format is an extension to /normal and /packed that puts a

target label "<target>=" in front of the (source) label in each step.

This target label overrides the order in which hypotheses are declared.

The /explicit formats will let you rearrange the ordering of $f and $e

hypotheses in the database without affecting any proofs.

The /packed and /explicit qualifiers aren't documented in the help yet.

The following examples illustrate all current proof formats:

MM> sh p ru/compressed

Proof of "ru":

---------Clip out the proof below this line to put it in the source file:

( vy cv wnel cab cvv wcel wn wceq wex wb wal pm5.19 df-nel

eleq12d notbid

eleq1 id syl5bb mtbir bibi12d a4v mto abeq2 nex isset mpbir )

ACZUHDZAEZF

DUJFGZHUKBCZUJIZBJUMBUMUHULGZUIKZALZUPULULGZUQHZKZUQMUOUSABUHULIZUNUQ ...

MM> sh p ru/normal

Proof of "ru":

---------Clip out the proof below this line to put it in the source file:

vx cv vx cv wnel vx cab cvv wnel vx cv vx cv wnel vx cab cvv wcel

wn vx

cv vx cv wnel vx cab cvv wcel vy cv vx cv vx cv wnel vx cab wceq...

MM> sh p ru/normal/explicit

Proof of "ru":

---------Clip out the proof below this line to put it in the source file:

vx=vx cA=cv vx=vx cB=cv wph=wnel vx=vx cA=cab cB=cvv wph=wnel

vx=vx cA=cv

vx=vx cB=cv wph=wnel vx=vx wcel.cA=cab wcel.cB=cvv wph=wcel

wps=wn vx=vx

cA=cv vx=vx cB=cv wph=wnel vx=vx wcel.cA=cab wcel.cB=cvv wph=wcel

vx=vy

wceq.cA=cv vx=vx cA=cv vx=vx cB=cv wph=wnel vx=vx wceq.cB=cab ...

MM> sh p ru/packed

Proof of "ru":

---------Clip out the proof below this line to put it in the source file:

vx 1:cv 1 2:wnel vx 3:cab cvv wnel 3 cvv 4:wcel wn 4 vy 5:cv 3

6:wceq vy

wex 6 vy 6 1 5 7:wcel 2 8:wb vx 9:wal 9 5 5 10:wcel 10 11:wn

12:wb ...

MM> sh p ru/packed/explicit

Proof of "ru":

---------Clip out the proof below this line to put it in the source file:

vx=vx 1:cA=cv cB=1 2:wph=wnel vx=vx 3:cA=cab cB=cvv wph=wnel

wcel.cA=3

wcel.cB=cvv 4:wph=wcel wps=wn wph=4 vx=vy 5:wceq.cA=cv wceq.cB=3

6:wph=wceq vx=vy wps=wex wph=6 vx=vy wph=6 wcel.cA=1 wcel.cB=5

7:wph=wcel

wps=2 8:wph=wb vx=vx 9:wps=wal wph=9 wcel.cA=5 wcel.cB=5

10:wph=wcel...

Here are the size and proof verification speed impacts of these formats

for set.mm (when all proofs are saved in the format):

/compressed: 'verify proof *' 14s, file size 28MB

/normal: 'verify proof *' 118s, file size 148MB

/normal/explicit: 'verify proof *' 4055s, file size 302MB

/packed: 'verify proof *' 20s, file size 36MB

/packed/explicit: 'verify proof *' 39s, file size 64MB

The 'verify proof *' time for /packed/explicit may vary depending on how

much hypothesis rearranging was done to in the database. The 39s

assumes no hypotheses were rearranged. Ordinarily, after editing the

hypothesis order as desired in the database, we would then 'save proof

*/compressed'.

The long run time for /normal/explicit might be improved somewhat with

more efficient code, but I don't think it will be used much so it

shouldn't matter.

Norm

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu