A number theory expression contains:
There exists at least one non-negative integer (written as E, existential quantifier)
All non-negative integers (written as A, universal quantifier)
+ (addition)
* (multiplication)
= (equality)
>, < (comparison operators)
&(and), |(or), !(not)
(, ) (for grouping)
variable names(all lowercase letters and numbers, not necessary one char long)
However, it has some more limitations:
- Arithmetic expressions should be syntactically valid. Here we only treat
+
as addition, not positive, so+
and*
should be surrounded by two number expressions - brackets should be well paired
<
=
>
should be surrounded by two number expressions&
|
!
are fed with logical expressionsE
andA
are fed with a variable and an expression- For
E
andA
, there should be a reasonable affected range. (*)
For (*): We write Ax Ey y>x & y=x
, Ax Ey y>x & Ey y=x
as well as Ax Ey y>x & Ax Ey y=x
, which mean Ax (Ey ((y>x) & (y=x)))
, Ax ((Ey (y>x)) & (Ey (y=x)))
and (Ax (Ey (y>x))) & (Ax (Ey (y=x)))
; however we don't write Ax Ey Ax x=y
or Ax Ey x<y & Ex x>y
. That means there should be some way to add brackets, so everywhere any variable is at most defined for once, and anywhere that use the variable has it defined.
Input
You'll be given an expression with these chars (invalid chars won't appear), only split when necessary (two variable names together), split after each quantifier variable, or each symbols are separated. No invalid symbol.
Output
Check whether it's a valid number theory expression. Either true/false or multi/one are allowed.
True samples (each symbol separated)
E a E b a < b
E b A x b < x & A x b > x
E b A x b < x & b > x
A b b + b < ( b + b ) * b | E x x < b
E x E y y < x & E x2 y = x2
E 1 A x x * 1 = x & E 2 2 * 2 = 2 + 2 & 2 > 1 & E x x + 1 = x * x * 2
E x E y y = y & y + y * y = y
False samples
E a E b a + b < c
E a E b b * ( a > a ) + b
A a A b ( a = b ) = b
A x A y A z A y x < z
E x E y y < x & E x y = x
E E x x = x
E x ( x < x
E x = x
Undefined behavior samples
E C C = C
AA x x = x
Ex = x
Shortest code in bytes win
Symbol definition: It's a resexpr
numexpr({s},∅) = s
numexpr(a∪b,c∪d) = numexpr(a,c) + numexpr(b,d)
numexpr(a∪b,c∪d) = numexpr(a,c) * numexpr(b,d)
numexpr(a,c) = ( numexpr(a,c) )
boolexpr(a∪b,c∪d) = numexpr(a,c) = numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) < numexpr(b,d)
boolexpr(a∪b,c∪d) = numexpr(a,c) > numexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) & boolexpr(b,d)
boolexpr(a∪b,c∪d) = boolexpr(a,c) | boolexpr(b,d)
boolexpr(a,c) = ! boolexpr(a,c)
boolexpr(a,c) = ( boolexpr(a,c) )
boolexpr(a-{s},c∪{s}) = E s boolexpr(a,c) if s∉c
boolexpr(a-{s},c∪{s}) = A s boolexpr(a,c) if s∉c
resexpr = boolexpr(∅,a)
a,b,c,d mean sets, s mean non-empty strings containing a-z0-9
Notes
- You don't need to check whether the expression is true, as it's usually impossible
numexpr(a,c)
, meaning "or" in BNF \$\endgroup\$