Click the example links in the Introduction to try them out! Syntax and semantics are described below.
This form will send your formula to the server.
To use tzimtsum locally, you can download the x86-64 Linux binary or compile the source code.
Have you ever wanted to know if there's a largest natural number?
There exists an x such that for all y, x is greater than or equal to y.
Or if a natural plus a positive natural could ever equal itself?
Let a = 0. There exist x, y for which y is greater than a and x plus y equals x.
Or if there are infinite even numbers?
For all x, there exists y that is larger than x and is two times some z.
Or if there exist x, y, z with n greater than 2 for which xn + yn = zn is satisfiable?
Well, tzimtsum can't help you with that last one. But it will let you decide the truth of any proposition involving quantifiers, addition, and comparisons (but not variable multiplication).
That's because Presburger arithmetic is a decidable theory, although the runtime is lower bounded by a double exponential in the number of nested quantifiers!
tzimtsum uses the automata-based solution given in Michael Sipser's Introduction to the Theory of Computation (6.2).
tzimtsum Syntax and SemanticsThe tzimtsum syntax is strict.
First, a series of quantifiers, either existential (E) or universal (A) and the variables they bind, separated by periods.
Then a series of literals (L), the variable it binds, an equals sign, and the natural number it binds to, separated by periods.
Then a formula using those variables and literals.
Be careful! Too many universals or too large of a formula will quickly grow too expensive to compute.
If a variable is not quantified over or bound to a literal, it defaults to zero.
tzimtsum accepts the following relations, which take in variables or literals and return a boolean.
- (<= a b) [true iff a is less than or equal to b]
- (< a b)
- (>= a b)
- (> a b)
- (= a b)
- (+ a b c) [true iff a plus b equals c]
- (+ a b c d)
- (not x)
- (and x y)
- (or x y)
- (if x y) [equivalent to (or (not x) y)]
tzimtsum is written in Haskell, and uses Parsec for parsing input. Interested readers can check out the source code, contributors welcome!
Comments and suggestions can be mailed to surya at [this domain name].
> In the magical art of Steganography, there is nothing frivolous, nor
contrary to the Gospels and the Catholic faith; nor have we taught
superstitious beliefs. Everything is based on natural, lawful and honest
principles; the mystery which veils the precepts of this art and the names
of the spirits, requires a cultivated reader; to hide the secrets of this
art, which could be harmful if made known to wicked men, we avail ourselves
of the services of the spirits.
tzimtsum is dedicated to my Friend, my Maybe Monad of Indiscriminate Embrace. Uniform Whiskey!