[SMT-LIB] Benchmark Conformance: log in AUFLIRA/nasa/

[cok@frontiernet.net]

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.

- 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