On 12 April 2017 at 13:12, Raymond <[email protected]> wrote: > For instance after > n : PI > we get. > > (9) -> if (n>-3) then true else false > > n is declared as being in PositiveInteger but has not been given a > value. > > This was also mentioned in: > http://axiom-wiki.newsynthesis.org/DefiniteIntegration > with no update (it's quite old) or response that I can see.. > "
What result would you expect from the following? n:Integer if n > -3 then true else false Should it return true or false? If you are willing to accept that in this case it could be either one, then the following might do something like what you expected in the case of PositiveInteger. n:PI if sample()$typeOf(n) > -3 then true else false But of course this could also be either true or false in a case such as if sample()$typeOf(n) > 3 then true else false Many domains export the sample() operation. It is guaranteed to return a value from the given domain but there are no promises made about what that value might be. Unfortunately this particular use of typeOf(n), where n has yet not been assigned a value, only works in the interpreter and in general you cannot pass variables to functions that do not have values. You can of course pass Symbol constants but that is something quite different. There is some other magic in the interpreter that allows you to treat definitions like x: Polynomial Integer and x: Expression Integer as if they had already been assigned values x:Expression Integer := 'x i.e. as generators. But be careful, do not be fooled by 'x:Expression Integer'. This does *not* mean that x is a variable that is somehow limited to Integer values. The Expression domain in FriCAS is a synonym for "rational function (ratio of polynomials) defined recursively over a fairly large number of "kernels", consisting of Symbols and other symbolic things like "sin(x)". In the type 'Expression Integer', 'Integer' refers to the coefficient domain of these polynomials. One may substitute any expression of the same type for x in a given expression, in addition to those expressions that consist of just an Integer constant. > n:PositiveInteger > > what this tells FriCAS is that n will be assigned an integer value > greater than 0 - only that. After it is actually assigned some value, > then it can be used exactly like that value, but not before. Strictly speaking in FriCAS 'n:PositiveInteger' does not say anything about assignment of values. What it tells you is exactly what operations are defined for objects of this type. You should think of types in "object-oriented" terms. FriCAS is a statically typed language so values in FriCAS do not have types, only the variables and functions have types. The reason that you can only assign integer values greater than 0 to objects of type PositiveInteger is because there are no legal operations available that would do otherwise. > > To me, this is a tremendous waste of an opportunity in FriCAS > to to deal with "domain of computation" issues such as are > addressed in other untyped computer algebra systems by the > use of "assumptions" such as: > > assume(x,PositiveInteger); > Your comment is a good excuse for a short rant ... I think what you call "domain of computation" is too ill defined to be treated in the way you suggest. FriCAS does however very carefully implement something else - the notion of "type" but I do not think that being typed or untyped has much to do with this issue. By domain of computation in this context I suppose you mean is something more specific like if forall(x:PI), x > -3 then ... or if exists(x:PI), x > 3 then ... in other words logical predicates with universal or existential quantification over some type. Resolving general expressions of this kind would require embedding FriCAS into some kind of theorem proving system. Some people (such as Tim Daly for example) seem to think this would be a good idea but in my opinion this goes against the idea of FriCAS/Axiom being an *algebraic* system. The design of the original Axiom system was fundamentally based on universal algebra ( https://en.wikipedia.org/wiki/Universal_algebra ), so the only form of logic that is really appropriate for FriCAS is equational logic ( http://www.cs.cornell.edu/gries/logic/Equational.html ). Rewrite rules are a form of equational reasoning. Internally FriCAS makes extensive use of such rules in the form of "automatic simplifications" that are applied during the process of evaluation to produce (nearly) canonical values for any expression. The rules that you have been using are a kind of extension of this. > I need it for a negative binomial rule/function as per: > https://arxiv.org/pdf/1105.3689.pdf > In GouldBK we never stoop so low as actually use numbers! :) There is a way to implement a kind of "assume" facility in FriCAS via equational reasoning that does not involve the type system. I have a proof of concept here: http://axiom-wiki.newsynthesis.org/SandBoxDomainOfComputation This is based in part of something else that I have been working on as part of improved support for symbolic computation in FriCAS. Bill. -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
