# Unicode ⊧ not an operator

**URL:** <https://discourse.julialang.org/t/unicode-not-an-operator/56698>\
**Category:** General Usage\
**Created:** [March 7, 2021, 9:18pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698 "2021-03-07T21:18:57Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![guyvdb](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/guyvdb/32/11596_2.png) [@guyvdb](https://discourse.julialang.org/u/guyvdb)\
**Post date:** [March 7, 2021, 9:18pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/1 "2021-03-07T21:18:58Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![stevengj](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stevengj/32/71_2.png) [@stevengj](https://discourse.julialang.org/u/stevengj)\
**Post date:** [March 7, 2021, 10:09pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/2 "2021-03-07T22:09:06Z")

</div>

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”)](https://www.fileformat.info/info/unicode/char/22a7/index.htm) was left out because it wasn’t clear to us at the time. Since it seems to be [only used in logic](https://en.wikipedia.org/wiki/Double_turnstile), 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?

---

<div class="post-metadata">

**Author:** ![guyvdb](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/guyvdb/32/11596_2.png) [@guyvdb](https://discourse.julialang.org/u/guyvdb)\
**Post date:** [March 7, 2021, 10:22pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/3 "2021-03-07T22:22:25Z")

</div>

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))

---

<div class="post-metadata">

**Author:** ![stevengj](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/stevengj/32/71_2.png) [@stevengj](https://discourse.julialang.org/u/stevengj)\
**Post date:** [March 7, 2021, 10:44pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/4 "2021-03-07T22:44:11Z")

</div>

> [@guyvdb](#):
>
> I believe it should have the same precedence as `≡` (\equiv):

`≡` 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.

---

<div class="post-metadata">

**Author:** ![guyvdb](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/guyvdb/32/11596_2.png) [@guyvdb](https://discourse.julialang.org/u/guyvdb)\
**Post date:** [March 7, 2021, 11:12pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/5 "2021-03-07T23:12:17Z")

</div>

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))

---

<div class="post-metadata">

**Author:** ![JeffreySarnoff](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/jeffreysarnoff/32/1980_2.png) [@JeffreySarnoff](https://discourse.julialang.org/u/JeffreySarnoff)\
**Post date:** [March 7, 2021, 11:56pm UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/6 "2021-03-07T23:56:32Z")

</div>

here are Julia’s  
[operator precedences](https://github.com/JuliaLang/julia/blob/master/src/julia-parser.scm)  
and

```julia
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)

```

---

<div class="post-metadata">

**Author:** ![o314](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/o314/32/252_2.png) [@o314](https://discourse.julialang.org/u/o314)\
**Post date:** [October 29, 2021, 1:47am UTC](https://discourse.julialang.org/t/unicode-not-an-operator/56698/7 "2021-10-29T01:47:09Z")

</div>

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 `=>`

```julia
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

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

```

quite natural , isn’t it?