Wow, great answer, thanks Mario! Mind duly blown.
The claim that contributors to mm files have in effect sorted the proofs in
a manner favorable to efficient verification should be scientifically
testable by the way (i.e. to a lower standard of 'proof' than what we're
used to around here). It's possible to write a program to shuffle an mm
file, the prediction being that makes verification a lot less efficient.
After that it might be possible to run some sort of regression on the
timings.
(I'm glossing over a lot of detail here, but a shuffle algorithm 1. makes a
pass of an mm file to construct a DAG, 2. writes out a random axiom, 3.
removes the axiom from the DAG which promotes any theorem no longer
dependent on any axioms to the status of axiom (though obviously still
outputted as a theorem), 4. return to step 2 until the whole file is
written out)
Best regards,
Antony
On Wed, May 11, 2022 at 5:21 PM Mario Carneiro <[email protected]> wrote:
> It's true that O(n) is an approximation of the reality. If you assume that
> array lookups can be done in O(1) (and there are at most 2^word size
> theorems total, which is almost certainly the case unless you have a
> "streaming" model for theorem verification, which is not the case for most
> proof systems), then you can get O(n) total time on a word RAM
> computational model. There is another asterisk though which is that
> theorems have to be O(1) in size for this to work. In general if theorems
> have size O(m) then verifying one metamath step takes O(m) so total
> verification time is O(mn), so in the worst case, if you have a single
> theorem whose statement takes up half of the entire file, you can spend the
> other half of the file applying that theorem O(n) times for O(n^2) work.
> This is the actual bound I have established for MM0 verification, but if
> you make a less pessimistic assumption it looks approximately linear.
> (There are also complications getting this linear time bound in metamath
> when *expressions* stop being O(1): you can actually get exponential size
> terms in O(n) steps by reusing subproofs. MM0 uses dag-like sharing of
> terms to circumvent this problem, but metamath fundamentally uses token
> strings for its expressions so you have to get fancy with data structures
> in order to express such a highly redundant string without losing the
> ability to freely reassociate token strings.)
>
> Setting aside the issues with large expressions and theorems and returning
> to the lookup question, the reality is still more complicated. If you don't
> use a word RAM model and instead use functional data structures, then your
> array is actually a tree and then you get that O(n log n) bound. If you
> remember The Myth of RAM (
> http://www.ilikebigbits.com/2014_04_21_myth_of_ram_1.html) then you will
> actually want to revise this to O(n sqrt n). But actually, it's a bit
> better than this because like regular programs, mathematics also has a lot
> of temporal and spatial locality, and this reflects in the fact that the
> theorems you access in the proof of a given theorem will often be hit many
> times and nearby theorems will also likely be accessed. So the usual
> caching tricks work and it goes down to O(n sqrt s) where s is the working
> set size, which is difficult to quantify but general considerations of how
> humans work suggest that this should be roughly constant - each area of
> mathematics generally has direct connections to O(1) other areas of
> mathematics. So we're back to O(n) again.
>
> Mario
>
> On Wed, May 11, 2022 at 7:37 AM Antony Bartlett <[email protected]> wrote:
>
>> Great talk Mario! Thanks for sharing.
>>
>> I nearly asked a couple of nights ago when it turned out Glauco and I
>> have both accidentally written Metamath verifiers in TypeScript which
>> probably run in O(n^2), hopefully on our way to writing verifiers that are
>> actually useable! What's a 'good' length of time in big-O notation for a
>> verifier to run in?
>>
>> In your talk you state that this is O(n) - unless I've wildly
>> misunderstood.
>>
>> I'm pleasantly surprised by that, and also curious. The best I was
>> hoping for was O(n.log(n)), and my thinking was that as you add more proofs
>> to the system, subsequent proofs sometimes refer back to them, which
>> requires the verifier to do a look up, which is why I was assuming 'n' to
>> make your pass of the file, and 'log(n)' for the lookups. Broadly, how
>> does an O(n) verifier avoid the need for this, please?
>>
>> Best regards,
>>
>> Antony
>>
>>
>> On Wed, May 11, 2022 at 11:03 AM Mario Carneiro <[email protected]>
>> wrote:
>>
>>> Hi all,
>>>
>>> I finally put the recording of my talk "Lessons from Metamath" from the
>>> Lorentz Center meeting for Machine-Checked Mathematics on YouTube. It is
>>> primarily aimed at an audience of people who are familiar with proof
>>> assistants but not with Metamath, but I'm sure you all can get plenty out
>>> of it as well.
>>>
>>> https://www.youtube.com/watch?v=OOF4NWRyue4
>>>
>>> Mario Carneiro
>>>
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "Metamath" group.
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to [email protected].
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/metamath/CAFXXJSsoNfduP5TgNbDzPMQEfFYYc4aCRt0y2aPRFPn6sH8ZyQ%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/metamath/CAFXXJSsoNfduP5TgNbDzPMQEfFYYc4aCRt0y2aPRFPn6sH8ZyQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "Metamath" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to [email protected].
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/metamath/CAJ48g%2BCwN2q7qKqi5oh4WezRV75V%2BikgT9DJyT4_tbmO825yyQ%40mail.gmail.com
>> <https://groups.google.com/d/msgid/metamath/CAJ48g%2BCwN2q7qKqi5oh4WezRV75V%2BikgT9DJyT4_tbmO825yyQ%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/CAFXXJSuz8Q5Hxcu7U3iV6%3DU2KwwbWg6dhiJEVj5ZJSTHpayA_A%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CAFXXJSuz8Q5Hxcu7U3iV6%3DU2KwwbWg6dhiJEVj5ZJSTHpayA_A%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAJ48g%2BDNwi2KhpTfYh%2BgfSTYd%2BV33Qmr_hWNfLSn3O6OnfgBXQ%40mail.gmail.com.
