What, then, is truly valuable to Tau?

At its foundation, value begins with statements that are both consistent and satisfiable. Anything unsatisfiable is immediately rejected by the system, so the power lies in expressing knowledge that can stand firm under logical scrutiny.

As we know, self contradiction statements are considered "false" in the logical sense, as we have seen in my Pointwise Revision demo, and are eventually discarded.  https://youtu.be/7YiGYBP4kQ0

o2[t] = 0 && o2[t] = 1   (Unsatisfiable) Proposal Rejected.

Beyond isolated statements, value emerges through connections and implications between them. Once Tau reaches a critical mass of common-sense knowledge, explicit repetition becomes unnecessary. If one asserts, "all pets are cute," and another asserts, "cats are pets," Tau will automatically deduce, "cats are cute." In this way, meaning compounds through agreement and inference.

A further layer of value lies in the opinion map, which makes visible what questions people find interesting. Knowing the questions many minds seek to answer is already a step closer to finding gold. Just as a prospector ignores common stones to search for rare gems, a contributor who focuses on high-demand questions is naturally positioned for greater reward.

In parallel, there is immense value in behavioral blueprints—the "what to do" and "what not to do" constraints that emerge in the testnet production stage. As users experiment with different rules, Tau reveals their real-world effects, producing fresh insights never before tested. This process generates entirely novel knowledge.

Value also grows through refinement of ideas on the opinion map, where collaborative filtering and sharpening turn raw notions into clarified wisdom. And finally, Tau treasures formalized definitions and knowledge, from precise software specifications such as "what it means to be secure," to the formalization of scientific research and intellectual property. These elements together pave the way for higher-level automation—eventually even the dream of an "automatic businessman."

In essence, Tau values consistency, inference, curiosity, behavioral truth, refinement, and formalization. Each layer builds upon the other, creating an ecosystem where knowledge itself is the rare mineral, and those who learn how to mine it most effectively are the ones who thrive.

Pointwise Revision is a crucial mechanism within the Tau Language that enables software updates and self-amendment without requiring the entire program or specification to be rewritten from scratch. It works by logically combining new requirements with existing ones, prioritizing outputs that satisfy both the old and new specifications, and falling back to only the new if there's a contradiction, thereby ensuring maximal preservation of the previous behavior. This algorithm solves the general "belief revision" problem in the context of Tau's software specification language, which is otherwise considered unsolvable.

Watch the Full Movie here: https://youtu.be/Hf9SG1tQeaA

Timeline

0:41 Part 1: Original Rule
8:20 Part 2: Proposed Rule (Accepted)
14:40 Part 3: Proposed Rule (Rejected)
21:25 Part 4: Proposed Rule (Accepted) Old - New
28:49 Part 5: Key Future Applications
34:33 Part 6: Short Quiz (Test Our Knowledge)
47:10 Part 7: Key Mechanism

Study Materials:

Atomless Boolean Algebras (Algorithms and Applications)
https://youtu.be/lNU1wS5rqtg

Theories and Applications of Boolean Algebras
https://tau.net/Theories-and-Applications-of-Boolean-Algebras-0.29.pdf

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

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 😊

When you want to actually write your input in real time and actually see the output also in real time, use console. This is helpful for me when I want interact in real time with Tau Language. I want to actually type the value on the REPL and I want to see what will be the output.

So this is how to write it

# Define your input
tau> sbf i1 = console

#Define your output
tau> sbf o1 = console

Now, you can input your value (0 or 1) and can see the actual output in the REPL

I will use some part of taumorrow's example in this link https://github.com/taumorrow/tau-lang-demos/blob/master/logic_gates.tau

Thank you l0g1x for providing the code for us.

But I change the input and output file format to console because I want to actually type the input myself and see the output results at an instant.

# Define input files
sbf i1 = console
sbf i2 = console

# Define output files
sbf o1 = console

# AND gate
r o1[t] = i1[t] & i2[t]

Please see below how we can use the Tau interpreter to multiply two 8bit numbers. Of course it can be easily extended to handle more bits, the important thing to remember is to keep the input file, called here "mask.in", filled with 0s (zeros) - to be exact double the amount of the input numbers' bits. So for this 8bits demo there should be 16 rows of 0s in "mask.in" file.

# a = 213 (11010101)
a8() := 1 # MSB
a7() := 1
a6() := 0
a5() := 1
a4() := 0
a3() := 1
a2() := 0
a1() := 1 # LSB
# b = 170 (10101010)
b8() := 1 # MSB
b7() := 0
b6() := 1
b5() := 0
b4() := 1
b3() := 0
b2() := 1
b1() := 0 # LSB

r_adder() := o2[0]=i1[0]+i2[0] && o2[t]=o1[t]+i1[t]+i2[t] && o1[t]=(i1[t-1]|i2[t-1])o1[t-1] | i1[t-1]i2[t-1]
init(x8,x7,x6,x5,x4,x3,x2,x1) := o0[0]=x1 && o0[1]=x2 && o0[2]=x3 && o0[3]=x4 && o0[4]=x5 && o0[5]=x6 && o0[6]=x7 && o0[7]=x8 && o1[t]=i0[t]

sbf i0=ifile("mask.in") # For multiplying 8bit numbers the mask file should have 16 zeros.
sbf o0=ofile("n1.in")
sbf o1=ofile("tmp0.out")
r init(a8(),a7(),a6(),a5(),a4(),a3(),a2(),a1())
sbf o0=ofile("n2.in")
r init(b8(),b7(),b6(),b5(),b4(),b3(),b2(),b1())

part1(x) := (x=1) ? (o1[t]=i1[t]) : (o1[t]=i0[t])
part2(x) := (x=1) ? (o1[t]=i1[t-1]) : (o1[t]=i0[t-1])
part3(x) := (x=1) ? (o1[t]=i1[t-2]) : (o1[t]=i0[t-2])
part4(x) := (x=1) ? (o1[t]=i1[t-3]) : (o1[t]=i0[t-3])
part5(x) := (x=1) ? (o1[t]=i1[t-4]) : (o1[t]=i0[t-4])
part6(x) := (x=1) ? (o1[t]=i1[t-5]) : (o1[t]=i0[t-5])
part7(x) := (x=1) ? (o1[t]=i1[t-6]) : (o1[t]=i0[t-6])
part8(x) := (x=1) ? (o1[t]=i1[t-7]) : (o1[t]=i0[t-7])

sbf i1=ifile("n1.in")
sbf i2=ifile("n2.in")
sbf o1=ofile("part1.out")
r part1(b1())
sbf o1=ofile("part2.out")
r part2(b2())
sbf o1=ofile("part3.out")
r part3(b3())
sbf o1=ofile("part4.out")
r part4(b4())
sbf o1=ofile("part5.out")
r part5(b5())
sbf o1=ofile("part6.out")
r part6(b6())
sbf o1=ofile("part7.out")
r part7(b7())
sbf o1=ofile("part8.out")
r part8(b8())

sbf o1=ofile("carry.out")

sbf i1=ifile("part1.out")
sbf i2=ifile("part2.out")
sbf o2=ofile("tmp1.out")
r r_adder()
sbf i1=ifile("tmp1.out")
sbf i2=ifile("part3.out")
sbf o2=ofile("tmp2.out")
r r_adder()
sbf i1=ifile("tmp2.out")
sbf i2=ifile("part4.out")
sbf o2=ofile("tmp3.out")
r r_adder()
sbf i1=ifile("tmp3.out")
sbf i2=ifile("part5.out")
sbf o2=ofile("tmp4.out")
r r_adder()
sbf i1=ifile("tmp4.out")
sbf i2=ifile("part6.out")
sbf o2=ofile("tmp5.out")
r r_adder()
sbf i1=ifile("tmp5.out")
sbf i2=ifile("part7.out")
sbf o2=ofile("tmp6.out")
r r_adder()
sbf i1=ifile("tmp6.out")
sbf i2=ifile("part8.out")
sbf o2=ofile("added.out")
r r_adder()



Thanks for l0g1x who gave me the idea how to work this out.


sudo apt-get update
sudo apt-get install libz3-dev

in this way we can install the z3.

Thanks l0g1x.

Hi guys, after for some weeks day off, I try to play again with the Tau REPL. I need to update it but some problem emerge. Now I delete the whole Tau folder. Then download again from the github website.

Now, I repeat the process I know on how to start by

1.) git clone https://github.com/IDNI/tau-lang.git
2.) cd tau-lang
3.) ./release.sh

but after, some error emerge, something to do with Z3-NOTFOUND



any idea how to get over this problem?

Please see below a significantly quicker version due to the arithmetic update (addition is now performed on bits) and introduction of leq function:

overflow(0) := 0
succb(u[15]()) := overflow(1)
succb(overflow(1)) := overflow(1)
succb(bin(b,c,d,e)) := bin(b+(cde),c+(de),d+e,e')
u[0]() := bin(0,0,0,0)
u[t]() := succb(u[t-1]())
addb(x|overflow(1),y) := overflow(1)
addb(overflow(1),x) := overflow(1)
addb(bin(b,c,d,e),bin(n,o,p,q)) := bin(b+n+(co|(d|p)(c|o)eq|(c|o)dp),c+o+(dp|(d|p)eq),d+p+(eq),e+q) | overflow(1) & (bn|(c|o)(d|p)(b|n)eq|(b|n)(c|o)dp|(b|n)co)
predb(bin(b,c,d,e)) := bin(b+(c|d|e)',c+(d|e)',d+e',e')
mulb(bin(0,0,0,0),x) := bin(0,0,0,0)
mulb(x,bin(0,0,0,0)) := bin(0,0,0,0)
mulb(overflow(1),x) := overflow(1)
mulb(x,overflow(1)) := overflow(1)
mulb(bin(b,c,d,e),bin(n,o,p,q)) := addb(mulb(predb(bin(b,c,d,e)),bin(n,o,p,q)),bin(n,o,p,q))
cmp(x,overflow(1)) := 0
cmp(bin(b,c,d,e),bin(b,c,d,e)) := 1
cmp(bin(b,c,d,e),bin(n,o,p,q)) := 0
leq(x,overflow(1)) := 0
leq(overflow(1),x) := 0
leq(y|overflow(1),x) := 0
leq(bin(b,c,d,e),bin(n,o,p,q)) := (n'b|(o'c)(nb|n'b')|(p'd)(oc|o'c')(nb|n'b')|(q'e)(pd|p'd')(oc|o'c')(nb|n'b'))'
oksq(x,q) := succb(x) & leq(mulb(succb(x),succb(x)),q)
okmul(x,y,q) := succb(y) & leq(mulb(x,succb(y)),q)
notpr1(q,0) := 0
notpr1(q,bin(b,c,d,e)) := notpr2(q,bin(b,c,d,e),bin(b,c,d,e)) | notpr1(q,oksq(bin(b,c,d,e),q))
notpr2(q,x,0) := 0
notpr2(q,x,bin(b,c,d,e)) := cmp(q,mulb(x,bin(b,c,d,e))) | notpr2(q,x,okmul(x,bin(b,c,d,e),q))
fndprm(x,prm[1]()) := 0
fndprm(x,prm[t]()) := (notpr1(x,u[2]()))'&prm[t]() | fndprm(predb(x),prm[t-1]())
primes(max[t]()) := fndprm(u[t](),prm[t]())

n primes(max[15]())


I implemented a simple prime numbers sieve within a 4 bits arithmetic in Tau. Feel free to post any improvements or modifications here.
And now for the code, it has two sections - I called them modules.
First is the implementation of the arithmetic with binary addition and multiplication, followed by the prime numbers generator section. See below:

#### 4-bit arithmetic module ####
succb(u[15]()) := overflow(1)
succb(overflow(1)) := overflow(1)
succb(bin(b,c,d,e)) := bin(b+(cde),c+(de),d+e,e')
overflow(0) := 0
ovf0(overflow(1)) := 0
ovf0(bin(b,c,d,e)) := 1
cmp(x,overflow(1)) := 0
cmp(bin(b,c,d,e),bin(b,c,d,e)) := 1
cmp(bin(b,c,d,e),bin(n,o,p,q)) := 0
u[0]() := bin(0,0,0,0)
u[t]() := succb(u[t-1]())
addb(overflow(1),x) := overflow(1)
predb(bin(b,c,d,e)) := bin(b+(c|d|e)',c+(d|e)',d+e',e')
addb(bin(0,0,0,0),x) := x
addb(x,bin(0,0,0,0)) := x
addb(bin(b,c,d,e),bin(1,1,1,1)) := overflow(1)
addb(bin(b,c,d,e),bin(n,o,p,q)) := addb(predb(bin(b,c,d,e)),succb(bin(n,o,p,q)))
mulb(bin(0,0,0,0),x) := bin(0,0,0,0)
mulb(x,bin(0,0,0,0)) := bin(0,0,0,0)
mulb(bin(b,c,d,e),bin(n,o,p,q)) := addb(mulb(predb(bin(b,c,d,e)),bin(n,o,p,q)),bin(n,o,p,q))
#### ENDof 4-bit arithmetic module ####


#### prime numbers module ####
oksq(x) := succb(x) & ovf0(mulb(succb(x),succb(x)))
okmul(x,y) := succb(y) & ovf0(mulb(x,succb(y)))
notpr1(u,0) := 0
notpr1(u,bin(b,c,d,e)) := notpr2(u,bin(b,c,d,e),bin(b,c,d,e)) | notpr1(u,oksq(bin(b,c,d,e)))
notpr2(u,x,0) := 0
notpr2(u,x,bin(b,c,d,e)) := cmp(u,mulb(x,bin(b,c,d,e))) | notpr2(u,x,okmul(x,bin(b,c,d,e)))
fndprm(x,prm[1]()) := 0
fndprm(x,prm[t]()) := (notpr1(x,u[2]()))'&prm[t]() | fndprm(predb(x),prm[t-1]())
primes(max[t]()) := fndprm(u[t](),prm[t]())
#### ENDof prime numbers module ####

#### prime numbers demo ####

n primes(max[15]())



I added gt and lt functions to my previous demo (note that a predecessor relation is also required for these, added as well - it's called "pred" here).

cmp(int[x](1),int[x](1)):=T
cmp(int[x](1),int[y](1)):=F
pred(int[t](1)):=int[t-1](1)
gt(int[0](1),int[x](1)):=F
gt(int[x](1),int[x](1)):=F
gt(x,y):=cmp(pred(x),y) || gt(pred(x),y)
lt(int[x](1),int[x](1)):=F
lt(int[x](1),int[y](1)):=gt(int[y](1),int[x](1))

So now we can also check whether a shape has more/less sides than the other:

sides(sqr()):=int[4](1)
sides(tri()):=int[3](1)
sides(rect()):=int[4](1)
greater(x,y):=gt(sides(x),sides(y))
less(x,y):=lt(sides(x),sides(y))

n greater(tri(),sqr())
n greater(sqr(),tri())
n greater(tri(),tri())
n greater(sqr(),sqr())
n greater(tri(),rect())
n greater(rect(),tri())
n greater(rect(),sqr())

n less(tri(),sqr())
n less(sqr(),tri())
n less(tri(),tri())
n less(sqr(),sqr())
n less(tri(),rect())
n less(rect(),tri())
n less(rect(),sqr())