Tau Forum

TL;DR:
While studying the Barber Paradox demo in Tau, I noticed that x = y' and x + y both produce XOR truth tables, suggesting they're logically equivalent (≡), but they normalize differently in Tau and behave differently in specs. I'm exploring whether this is a syntax limitation or a deeper design choice in Tau logic.

I was studying the Barber Paradox Demo from the Tau GitHub repo:

barber_demo_2.tau (https://github.com/taumorrow/tau-lang-demos/blob/master/barber_demo_2.tau)

1. First Formula

barber1(x, y) := x = y'
Tau RELP output:

barber1(x, y) := x'y' | xy = 0
Truth Table (looks like XOR):

x   y   x'    y'    x'y'     xy     x'y' | xy    x'y' | xy = 0 0   0   1    1     1      0          1             0 0   1   1    0     0      0          0             1 1   0   0    1     0      0          0             1 1   1   0    0     0      1          1             0

Normalized form:

n = x=y'   →  xy=0 && x'y'=0
Truth Table (looks like XOR):

x   y   x'   y'   x'y'    xy    xy=0   x'y'=0   xy=0 && x'y'=0 0   0   1   1    1     0      1              0                    0 0   1   1   0    0     0      1              1                    1 1   0   0   1    0     0      1              1                    1 1   1   0   0    0     1      0              1                    0

2. Second Formula (Alternative)

barber2(x, y) := x + y
Tau RELP output:

barber2(x, y) := x'y|xy'
Normalized form:

n = x + y   →    xy' | x'y
Truth Table (also looks like XOR):

x   y   x'   y'   x'y   xy'   x'y | xy' 0   0   1   1    0   0       0 0   1   1   0    1   0       1 1   0   0   1    0   1       1 1   1   0   0    0   0       0

❓Observation & Question

The two expressions:

x = y'  ≡  x + y
...appear logically equivalent (same truth table, both represent XOR), yet they normalize differently and behave differently in Tau logic. For example:

barber2(x, y) := x + y
paradox(b)→ (Error) Type mismatch. barber2[0]/2() : bf declared as wff

Using + (as an XOR) seems accepted in some places but not in others. I also tried ^ but that gave a syntax error.

🔎 My Hypothesis

It seems:

Using := expects a term on the right-hand side (not a Tau spec).

Even though x = y' and x + y are logically equivalent in Boolean logic, Tau's syntax might treat them differently due to the parsing rules or term/spec expectations.

💬 I'd love to hear your thoughts!

• Is there a reason Tau doesn't normalize x + y the same as x = y'?
• Is this a syntax limitation, or is there a deeper logical distinction being modeled?
• Any tips for handling XOR equivalence in Tau definitions?

Note:
I use the symbol ≡ to mean logically equivalent, i.e., expressions that always produce the same truth values across all inputs.

Thanks in advance for any insights!

— Still learning Tau 😊