The answer is that I am using BooleanConvert, but needed an alternative version:
ANFtoArith[fun_] := With[{fun2 = Replace[ReplaceRepeated[
fun, {x_ && y_ :> x*y, ! x_ :> x + 1,
x_ \[Xor] y_ :> x + y, False -> 0, True -> 1}],
{Function[x_] :> Mod[Expand[x], 2]}]}, Function[fun2]]
f2sBool = BooleanConvert[BooleanFunction[#], "ANF"] & /@ Tuples[{0, 1}, 2^2];
f2sArith = ANFtoArith /@ f2sBool
Out[]={0 &, Mod[1 + #1 + #2 + #1 #2, 2] &, Mod[#2 + #1 #2, 2] &,
Mod[1 + #1, 2] &, Mod[#1 + #1 #2, 2] &, Mod[1 + #2, 2] &,
Mod[#1 + #2, 2] &, Mod[1 + #1 #2, 2] &, Mod[#1 #2, 2] &,
Mod[1 + #1 + #2, 2] &, Mod[#2, 2] &, Mod[1 + #1 + #1 #2, 2] &,
Mod[#1, 2] &, Mod[1 + #2 + #1 #2, 2] &, Mod[#1 + #2 + #1 #2, 2] &, 1 &}
The full story is kind of funny actually... I got into metamath relatively late, actually at the very end. The assumption seemed to be "oh this guy is a physicist, what could he possibly know". Well, for one, "circuit design" and Boolean logic. They had a proof of De Morgan's theorem on the record I think it was taking hundreds of steps and I said, "No, it's just one step, Expand[...]":
Mod[Expand[ANFtoArith[And[Not[#1], Not[#2]]] @@ {a, b}], 2]
ANFtoArith[BooleanConvert[BooleanFunction[{0, 0, 0, 1}], "ANF"]] @@ {a, b}
Out[47]= Mod[1 + a + b + a b, 2]
Out[48]= Mod[1 + a + b + a b, 2]
There was probably another implication that I was too small minded to fully understand the notion of how to count operations, but I also did some Bernstein-style analysis breaking down Expand to more elemental logic or arthmetic functions and counting repeated usages up to forty or fifty at max, not hundreds.
SW asked for this to be developed for WFR, then someone else demoted it to a Hobby project in his official notes. If the disagreement gets any bigger I guess we will have to ask Thomas Hales.
For now the priority is relatively low with hopes to have some more done by July, but generalizing ANF to other radix looks to be really not that easy, perhaps explaining why it isn't in NKS (but should be). If we figure it out, in the end, we could have a more powerful, more general version of BooleanConvert,
which arguably could follow into the kernel.
Yea I agree find patterns in the pictures could be a way forward, but another issue I'm worried about is possible multiple solutions. Is there exactly one way to "functionalize a truth table", or do we need to worry about canonical choosing?
