shadowing doesn't work for <, and leads to inconsistency for interpreted <

[erniecohen]

The language manual seems to say that, aside from being polymorphic, relations like < behave like other relations. However, they don't seem to shadow properly. For example:
#lang ivy1.7
type s
type t
relation lt(T:t,T1:t)
axiom X:s=0 -> X < 1
axiom X:t=0 -> lt(X,1)
object o = {
relation (S:s < S:s) # this should shadow the outer < on s
relation lt(T:t,T:t) # this does shadow the outer lt on t
action testS = { var x:s; assert x=0 -> x < 1 } # succeeds (but should fail)
action testT = { var x:t; assert x=0 -> lt(x,1) } # fails (as it should)
}

Proper shadowing for built in relations is useful, as it allows theories over a single relation to be written using built in relational symbols and instantiated with non-relational symbols without having to commit the type being axiomatized to using that symbol with the same meaning.

The lack of proper shadowing for interpreted types also leads to inconsistency (though perhaps this is really a different issue):
#lang ivy1.7
type nat
interpret nat->nat
relation (N:nat < N:nat)
definition (N:nat < N1) = true
invariant X:nat<X
invariant false

[kenmcmil]

Your second example is an Ivy bug. That is, you shouldn't be able to define an interpreted symbol.

The syntax relation (X:t < Y:T) ought to be deprecated in version 1.7 of the language, since this symbol is implicitly declared for every type.

I'm not sure what you mean by instantiating a relational symbol with a non-relational symbol. That would be a type error in Ivy. Can you give an example of a use case?

[kenmcmil]

The bug with definition of interpreted symbols is fixed in commit 3477e94. Ivy now gives an error message for this.

[erniecohen]

I'm sorry, instead of "non-relational", I meant to say "non-built-in".

I disagree with the deprecation of explicit built-in symbol declaration. I think built-in relational symbols should follow the same rules as other symbols, except for being implicitly declared whenever you declare a type. That is, you should be able to redefine them locally, creating a shadow.

For example, suppose you have a type with two partial orders. For example, strings are ordered both lexicographically and by prefix. We want to use the ordering library to, say, axiomatize that the lexicographic ordering is a linear order and that the prefix order is a partial order. If you fix the interpretation of < on that type, you can't use the ordering library to talk about the other one.

What you want to do is to pass the two relations into two instances of the ordering definitions. Ideally, you would do that by passing the relation in and the modules using "<" as a parameter. In the absence of that, you would use an ordinary parameter and introduce (in the ordering definition) a local "<" defined to be equal to the parameter. This "<" definition would override the surrounding definition.

[erniecohen]

I forgot to mention: explicitly defined "<" would still have to be homogeneous, so you know which of the polymorphic "<" symbols you are overriding.

[kenmcmil]

I see. I think there are two issues here. First, are you allowed to define a relation foo.<? I'm not sure whether I like that or not. For example, would it be infix or prefix? I'll think about it. The other issue is making the theory modules parametric on the relation symbol. This you can already do:

#lang ivy1.7

module totally_ordered(t,r) = {
    property [transitivity] (r(T:t,U) & r(U,V)) -> r(T,V)
    property [antisymmetry] ~(r(T:t,U) & r(U,T))
    property [totality] r(T:t,U) | T=U | r(U,T)
}

type t

instantiate totally_ordered(t,<)

interpret t -> nat

So maybe there should be such modules in the standard library.

Another idea: allow subscripts on the built-in symbols, so you can use both orders in the same context.

[kenmcmil]

On reflection, I think I would rather not support overriding of the polymorphic symbols. As things are, elaboration of modules and objects is orthogonal to type inference, and I think I would like to keep it that way. So if you want to override, you have to use a monomorphic symbol. It should be possible to override built-in monomorphic symbols, but I think the only one of those is bool, which would be a bit scary to override.