Clean up section on cyclers

bbchallenge / bbchallenge-proofs

Mathematical proofs of the bbchallenge project.

Creative Commons Attribution 4.0 International

16 stars 6 forks source link

Clean up section on cyclers #13

Closed int-y1 closed 11 months ago

int-y1 commented 11 months ago

Big changes:

Algorithm 1, line 8: Change initial state to 1, because state A is represented as 1.
2.2 Correctness: Use $i$ and $j$ to represent indices, and update proofs.

Small changes:

Algorithm 1, line 11: Change to "currTime $\leq$ timeLimit" so that the decider tries to find duplicates within $c_0, c_1, c_2, \dots, c_t$.
2.1 Pseudocode: Mention Algorithm 1. (Algorithm 1 didn't appear between 2.1 and 2.2)
Various typo fixes.

UncombedCoconut commented 11 months ago

Thanks! These changes look good to me. (Nit: I thought the paper did enumerate state A as 0? The seed DB is where it's 1-based. This is easily addressed after merging, and maybe the pseudocode can just let "A" refer to the correct constant.)

I'll allow time for tcosmo to review.

meithecatte commented 11 months ago

I'm opposed to representing states as integers in the paper. We should consider them as an abstract data type with five values called A through E.

UncombedCoconut commented 11 months ago

I'm opposed to representing states as integers in the paper. We should consider them as an abstract data type with five values called A through E.

This is my preference as well. (At least: abstract type, distinguished "A", "for each state" is a valid loop.) Thus it's also my preference to merge this PR and adopt that style afterward.

tcosmo commented 11 months ago

I'm opposed to representing states as integers in the paper. We should consider them as an abstract data type with five values called A through E.

Agreed!

Thank you @int-y1 for your changes, all looks good!