[SMT-LIB] overloading and type checking.

[cok@frontiernet.net]

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.  So I would in general be in favor of user overloading by rank and argument type, but not by return type; however, I don't at all consider it an essential change, and acknowledge all the discussion and concerns raised previously that Cesare referred to.

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

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