On Thursday, April 13, 2017 at 9:16:37 PM UTC-4, Bill Page wrote: > > On 12 April 2017 at 13:12, Raymond <[email protected] <javascript:>> > 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. > So as of now: If in combinatorial deduction I end up descending through formulas with conditions attached a>b ,c>0 , d<=c and I want them to be usable for other calculations or display; I should do something like: make a property list, associated with the variable, that contains the acquired conditions and refer to that list when testing/reading _values_ . This is fine, in combinatorics it seems that every question has a multi-valued answer: yes, no, maybe, perhaps, well if, .... One of my concerns is making a deduction without knowing the restrictions imposed by the rules used; when those rules are invoked by other rules. Type declarations are for operators not values. BTW: thanks for explaining it in some detail and I hope I have finally understood a little "under the hood".
-- 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.
