>
> Bill Page wrote:
>> Although something like this has been done in other computer
>> algebra systems I am not convinced that implementing "provisos"
>> or any other type of "conditional expression" is a good direction
>> for FriCAS. FriCAS is fundamentally a strongly-typed *algebraic*
>> system but it seems to me that the concept of conditional
>> expressions leads in another direction involving symbolic
>> manipulation and logic.
>>
>
On Wed, Dec 3, 2008 at 8:59 PM, Waldek Hebisch wrote:
> IMHO we need all of them: algebraic part, symbolic manipulation,
> logic and numerical computations. Refusing promising approach
> on ideological reasons would be very wrong precedent.
>
Ok. I agree that "ideological reasons" alone would not be sufficient
to argue against any given possible approach. But I am quite convinced
that one of the strengths of FriCAS (alias Axiom) is the ways in which
it differs from other current computer algebra systems. For me it is
the strongly typed algebraic-oriented language of FriCAS that sets it
apart and makes it of great interest to me. Of course this is viewing
FriCAS as a research-oriented platform rather than as a merely a tool
for doing mathematics by computer but I think there are other open
source options available for simply "doing mathematics by computer"
that are already significantly more advanced than FriCAS and FriCAS
has very little possibility to "catch-up" with these developments.
>
>> It seems to me that just having conditional expressions is not
>> enough. In evaluating conditions it is necessary to know which
>> symbols are parameters and which are constants.
>
> What is the difference between constant and parameter? AFAICS
> there is no need to distinguish unknown constant and a parameter.
>
Consider a constant such as
(1) -> x::Polynomial(Integer)
(1) x
Type: Polynomial(Integer)
>> Maybe what you are suggesting
>> could be represented by a domain for piecewise defined functions.
>> Something like this is already possible in the interpreter:
>>
>> It seems to me that a better direction for FriCAS would be to
>> insist that this sort of logic remain part of the *type system*
>> of the language rather than as values in some new "conditional
>> expression" domain. I believe that this was one of the original
>> motivations for the concept of the "SubDomain" constructor:
>> ...
>
> Conditional expressions are realistic appraoch: possibly as
> little as a week of coding can give useful implementation.
Given how (relatively) unsuccessful this approach has been in other
computer algebra systems I have doubts about this claim, but if you
can prove me wrong I would of course be very interested in the result.
> Using type system for this is a speculation and even at level
> of speculation is not very promising. Namely, one reason we
> need conditions is that our mathematical algorithms are too
> weak to give unconditional answer.
I believe that in many cases it is not a matter of "weakness" of the
algorithms but rather an inherent feature of the nature of these
answers. In a strongly-typed system like FriCAS it makes sense to me
that this should be reflected in the underlying type system that
qualifies such values as belonging to specific domains. I tried to
provide what I thought was a good example of this in dealing with
multiple-valued functions as defined over "Riemann surfaces"
represented by a Union of repeated domains.
> The other is when result have "discontinuous" dependence
> on parametes -- more precisely result can not be captured by
> single formula. Both reasons means that conditions are a
> runtime thing and as we refine implementation we will want
> to use deep mathematical knowledge to handle them.
> OTOH our types are quite heavy at runtime and type checker
> has only little mathematical knowledge (basicaly rather simple
> minded support for propositional calculus). Strength of type
> checker is static checking, but actually to benefit from static
> checking conditions have to be _data_ (because static type
> checking of types is actually weaker than static type checking
> of ordinary data).
>
I think that the existence of dependent types considerably modifies
the situation as you describe it above. Of course SPAD does not fully
implement dependent types - at least not as completely as done say by
Aldor. Still SPAD does have many features that make it's type system
more powerful than you imply. For example, the 'has' predicate
certainly involves more than "simple minded support for propositional
calculus".
DirectProductCategory(dim:NonNegativeInteger, R:Type): Category ==
Join(IndexedAggregate(Integer, R), CoercibleTo Vector R, _
finiteAggregate) with
directProduct: Vector R -> %
if R has SetCategory then FullyRetractableTo R
if R has Ring then ...
if R has AbelianSemiGroup then AbelianSemiGroup
>
> SubDomain nicely illustates this point: because cond is a
> function typechecker can do nothing beyond checking that
> cond takes values of declared type and returns Boolean.
>
I do not see this a limitation of the type system. It seems essential
and unavoidable to me that FriCAS must be able to evaluate
Boolean-valued functions that are part of a domain defined as a
SubDomain at run-time. Could you elaborate on how this illustrates
your point?
Regards,
Bill Page.
--~--~---------~--~----~------------~-------~--~----~
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en
-~----------~----~----~----~------~----~------~--~---
