[SMT-LIB] overloading and type checking.

[Cesare Tinelli]

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