Unicode ⊧ not an operator

I wondering if it’s worth filing an issue about the ⊧ unicode character: Julia supports entering it with \models but it cannot be used as either a variable or an operator (contrary to most other unicode math operator characters like ≡). I wonder if there is a good reason or someone forgot to add this one to the operator parsing table? I would love to use it as a function name for deciding logical entailment.

When we started parsing Unicode math symbols (category Sm) in Julia as infix operators, we had to manually decide on what precedence to assign each operator (or whether to allow them as infix at all). To be conservative, we left out any operator whose precedence was unclear — we can always add new symbols later without breaking backwards compatibility, but if we choose incorrectly we are stuck with it in Julia 1.x.

(U+2287 “Models”) was left out because it wasn’t clear to us at the time. Since it seems to be only used in logic, someone familiar with its usage can probably suggest a reasonable precedence.

Should it be the same as (\vdash) or (\implies), both of which are already infix operators (with differing precedence)? It seems that it can also be used as a unary operator?

3 Likes

Thanks! That makes sense. I believe it should have the same precedence as ≡ (\equiv): both express logical relationships between sentences. It should have a lower precedence than the logical connectives that are used to construct logical sentences.

So concretely
x ∨ y ∧ z ⟹ w ⊧ x ⊻ z
is parsed as
(((x ∨ (y ∧ z)) ⟹ w) ⊧ (x ⊻ z))

1 Like

has the same precedence as == and other comparison operators, which is higher precedence than that of (and other arrows). For example, x ∨ y ∧ z ⟹ w ≡ x ⊻ z is parsed as (x ∨ (y ∧ z)) ⟹ (w ≡ (x ⊻ z)). It doesn’t sound like this is what you want.

2 Likes

I see, that means I should probably not be using ≡ (or a future ⊧) in my API as logic users would expect the identity
x ⟹ y ≡ ¬y ⟹ ¬x
to be parsed as
(x ⟹ y) ≡ (¬y ⟹ ¬x)

In this context ≡ has a different precedence from =, for example the following statement is true in SMT(LRA) logic:
x>=5 ≡ x=5 ∨ x>5
because it gets parsed as
(x>=5) ≡ ((x=5) ∨ (x>5))

here are Julia’s
operator precedences
and

help?> Base.operator_precedence
  operator_precedence(s::Symbol)

 Return an integer representing the precedence of operator s,
 relative to other operators. Higher-numbered operators take
 precedence over lower-numbered operators.
 Return 0 if s is not a valid operator.

  Examples
  ≡≡≡≡≡≡≡≡≡≡

  julia> Base.operator_precedence(:+),
         Base.operator_precedence(:*), 
         Base.operator_precedence(:.)
  (11, 12, 17)

  julia> Base.operator_precedence(:sin),
           Base.operator_precedence(:+=),
           Base.operator_precedence(:(=))  
           # (Note the necessary parens on `:(=)`)
  (0, 1, 1)
1 Like

You can use the ascii |= operator for entailment
it’s a fabricated operator eg. an update-operator for | but it’s prec is the prec of = the lower recognized one


it will match the prec rule between |= and =>

using Test
@test (Base.operator_precedence(:|=) == 1) <=
                (Base.operator_precedence(:(=>)) == 2)


|= and => are the two loosely precedence one can get with ops. so &, | expr will go ‘inside’
x ∨ y ∧ z => w |= x ⊻ z) will be parsed as

Expr(:|=,
    Expr(:call, :(=>),
        Expr(:call, :∨, :x, Expr(:call, :∧, :y, :z)),
        :w),
    Expr(:call, :⊻, :x, :z))

quite natural , isn’t it?