[SMT-LIB] overloading and type checking.

Fri Nov 5 17:58:07 EDT 2010

Hi David, and all,

On 4 Nov 2010, at 02:54, cok at frontiernet.net wrote:

> I was more commenting than advocating a position. And I don't really want to advocate major changes in SMT-LIB, as it has gone through quite a bit of discussion and needs settling down; nevertheless, experience with a standard can inform future changes.
> 
> So, were I to advocate changes, this is what I would advocate:
> 
> - some degree of overloading (by rank and type) is necessary to have natural use of - + = etc.
> 
> - to me, if the background theory allows something (e.g. ad hoc and/or parameteric overloading) there is no increase in implementation complexity and a decrease in conceptual complexity for uses to be allowed to do the same thing.

This is actually not the case. It is in fact one of the main points of SMT that one uses specialized approaches to deal with the theories. General purpose facilities that extend theory-based functionalities to user-defined stuff do in general increase implementation complexity, if not conceptual one.
So I do not think that we could your the point about as a general principle.

>  So I would in general be in favor of user overloading by rank and argument type, but not by return type;

I presume this recommendation is is based on the fact that currently there are no theories with overloading by return type. If so, it seems a bit shortsighted. We certainly expect to increase the number of theories in SMT-LIB, as we have done over the years, to support more and more theories for which people have created specialized reasoners. And there are certainly theories out there that could make it to SMT-LIB which have symbols overloaded by return type.

Tjark has provided a important example in his reply. Injection functions for sum types show up in the theory of algebraic data types.

Another example is a version of the theory of arrays with array constant constructors, which have functions with signature  init: X -> array(Y,X)

> however, I don't at all consider it an essential change, and acknowledge all the discussion and concerns raised previously that Cesare referred to.
> 
All right.

> - if we are to have overloading by return type and the 'as' construct, I'd rather it be limited to constants
> 

See my comment above. 
In any case, I apologize but I do not understand what exactly the problem is with as. The only difference is that a symbol table contains a list of return sorts for each (function symbol, input sort list) pair, instead of a single sort. To determine the sort of ((as f t) a1 a2 a3) you has to determine the sort of a1, a2 and a3 first anyway. Once you have those, s1, s2, s3, say, you fetch from the symbol table the return sorts of f,s1, s2,s3 and verify that t is among them. Am I missing something?

Cheers,

Cesare

> David
> 
> ----- "Cesare Tinelli" <tinelli at cs.uiowa.edu> wrote:
> 
>> Hi David,
>> 
>> On 3 Nov 2010, at 09:33, cok at frontiernet.net wrote:
>> 
>>> I'll concede that the (as nil T) example is a useful motivation.
>>> However, for functions such as your general example
>>> f: t_1 ... t_n t  and  f: t_1 ... t_n t'
>>> with n > 0, I'd just want one of the f's to be renamed.  The
>> nuisance in type-checking is this.
>>> The expression one writes is
>>> ((as f t) a1 a2 a3)
>>> with values a1 a2 a3 (which have types t1 t2 t3)
>>> In such an expression there is no type for  (as f t) considering
>> only its components - one has to resolve ((as f t) t1 t2 t3) as a
>> unit.  Certainly doable, but a nuisance in the bottom-up model.
>>> 
>> 
>> I'm a bit confused here. You seem to be advocating the elimination of
>> 'as, while at the same time recommending the introduction of
>> overloading for user-defined symbols. How would the former simplify
>> bottom-up type-checking? In fact, it would make it impossible as far
>> as I can tell.
>> Are you perhaps suggesting to limit 'as only to constant symbols?
>> 
>> 
>> 
>> Cesare
>> 
>> 
>> 
>> 
>>> - David
>>> 
>>> ----- "Tjark Weber" <tjark.weber at gmx.de> wrote:
>>> 
>>>> On Wed, 2010-11-03 at 07:21 +0000, cok at frontiernet.net wrote:
>>>>> - We should however keep what can be done in a theory consistent
>>>>> with what can be done in other commands.  The fact that
>> overloading
>>>>> (with different ranks) can happen in one place and not the other
>> is
>>>>> a nuisance in parsing and inconvenient for the user.
>>>> 
>>>> I agree that overloading with different ranks -- since it can
>> happen
>>>> in
>>>> theories -- should perhaps be allowed for user-declared symbols as
>>>> well.
>>>> 
>>>> However, if overloading is allowed, the standard needs to specify
>> the
>>>> behavior in case the user attempts to overload a polymorphic
>> symbol
>>>> (such as 'store').  (Probably, it should be allowed if and only if
>>>> the
>>>> new rank is not an instance of the polymorphic rank.)
>>>> 
>>>>> - The overloading on return type with the 'as' construct appears
>> to
>>>>> have limited utility and also complicates the bottom up
>>>> typechecking.
>>>> 
>>>> My understanding is that 'as' is used if (and only if) there are
>>>> symbols
>>>> 
>>>> f: t_1 ... t_n t  and  f: t_1 ... t_n t'
>>>> 
>>>> with t <> t'.  In the absence of overloading, I am not sure how
>> one
>>>> would declare these -- only as theory symbols?  But assuming they
>>>> exist,
>>>> 'as' is a highly useful feature: without it, straightforward
>>>> bottom-up
>>>> type checking would no longer be possible.
>>>> 
>>>> The (as nil (List Int)) example (on page 24) motivates 'as' well,
>> in
>>>> my
>>>> opinion.
>>>> 
>>>> Regards,
>>>> Tjark
>>>> 
>>>> _______________________________________________
>>>> SMT-LIB mailing list
>>>> SMT-LIB at cs.nyu.edu
>>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>> _______________________________________________
>>> SMT-LIB mailing list
>>> SMT-LIB at cs.nyu.edu
>>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>> 
>> 
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib