[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut
hv at crypt.org
hv at crypt.org
Mon Oct 24 14:16:00 CEST 2022
I can imagine such output being of value - as an option of course,
not by default.
The opportunity to check a proof seems critical to me. The easier
it is to check, the greater the confidence we can have in the proof.
Hugo
Jeffrey Shallit <shallit at uwaterloo.ca> wrote:
:Just as a follow-up:Â a typical Walnut query consists of a parsable
:logical formula, for example
:something like
:
:For all x there exists y such that f(x,y) holds.
:
:But in Walnut it is easy to assert
:
:1.Â f(x,y) holds
:2.Â there exists y such that f(x,y) holds
:3.Â For all x there exists y such that f(x,y) holds.
:
:And get automata corresponding to each of these.Â Â So Walnut already has
:the capability to produce the
:automata for individual parts of any expression and these could be
:considered a certificate
:and each part could then easily be individually checked by another
:program, if one wanted.
:(But the other program would essentially just be reproducing the
:calculations of Walnut!)
:
:
:On 2022-10-24 8:19 AM, Jeffrey Shallit wrote:
:>
:>
:> On 2022-10-21 11:21 AM, hv at crypt.org wrote:
:>>
:>> While I know a little about DFAs from my programming work (including
:>> a lot of work on the regexp engine in Perl), I know little about them
:>> mathematically. Is it plausible that Walnut could generate a kind of
:>> certificate by outputting one or more DFAs along with some
:>> canonicalized description of the transformations it is performing
:>> on them?
:>>
:>>
:> Unfortunately that would be (for all practical purposes) just redoing
:> exactly the same
:> calculation that Walnut is already doing.Â Â And for some of them the
:> "certificate" would be really huge.
:>
:> So I don't see any point in doing that.
:>
:> --
:> Seqfan Mailing list - http://list.seqfan.eu/
:
:
:--
:Seqfan Mailing list - http://list.seqfan.eu/
More information about the SeqFan
mailing list