SMTLIB v3: polymorphism

[François Bobot]

Hi,

Just to follow on the question about polymorphism and disambiguation from the status report of the
SMT-LIB v3 at the SMT-Workshop. http://smtlib.cs.uiowa.edu/version3.shtml.


```
(declare-const f (par (X Y) (-> X Y)))

(declare-const f (par (X) (-> X X)))
```

How do you disambiguate in the case of (-> Int Int) ?

Thanks,

--
François

[Cesare Tinelli]

Hi François,

You win the race for the fastest feedback ever! 🙂

The informal description of the overloading policy is that, while a (possibly higher-order) constant symbol can be declared more than once, it cannot be redeclared with the same type. 

The meaning of this is clear for monomorphic constants. For the general case that includes polymorphic constants, the technical restriction is that the new type assigned to a constant c cannot have instances in common with one of the current types of c.

In your example, the second declaration would have to be rejected because 

(par (X) (-> X X))) is in fact an instance of 

(par (X Y) (-> X Y))) (obtained by instantiating the parameter Y with X).

Note, that the sequential order of the definition is immaterial to the acceptance of both: declaring f first to have type (par (X Y) (-> X Y))) precludes the possibility of declaring it with type (par (X Y) (-> X Y))) later.

I will clarify this issue on the webpage.

Thanks,

Cesare