[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut
shallit at uwaterloo.ca
Mon Oct 24 14:24:42 CEST 2022
Just as a follow-up: a typical Walnut query consists of a parsable
logical formula, for example
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/
More information about the SeqFan