[seqfan] Re: talk announcement: Proving properties of OEIS sequences with Walnut

[Jeffrey Shallit]

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/