On 05/15/2008 03:01 AM, Gabriel Dos Reis wrote:
> Ralf Hemmecke <[EMAIL PROTECTED]> writes:
>
> | On 05/14/2008 06:27 PM, Gabriel Dos Reis wrote:
> | > Ralf Hemmecke <[EMAIL PROTECTED]> writes:
> | > | On 05/14/2008 05:26 PM, Gabriel Dos Reis wrote:
> | > | > Waldek Hebisch <[EMAIL PROTECTED]> writes:
> | > | > | Gabriel Dos Reis wrote:
> | > | > | > | > The definition of the function recip$NormalizationPackage
> | > | > elicites
> | > | > | > a `semantic error' from the compiler because the local variable
> | > | > | > `hesrg' is defined in the two branches of an if-statement with two
> | > | > | > differen types. That looks like a bug to me. Opinion?
> | > | > | > | > recip(p:P,ts:TS): Record(num:P, den:P) ==
> | > | > | > -- ASSUME p is invertible w.r.t. ts
> | > | > | > -- ASSUME mvar(p) is algebraic w.r.t. ts
> | > | > | > v := mvar(p)
> | > | > | > ts_v := select(ts,v)::P
> | > | > | > if mdeg(p) < mdeg(ts_v)
> | > | > | > then
> | > | > | > hesrg: Record (gcd : P, coef2 : P) :=
> halfExtendedSubResultantGcd2(ts_v,p)$P
> | > | > | > d: P := hesrg.gcd; n: P := hesrg.coef2
> | > | > | > else
> | > | > | > hesrg: Record (gcd : P, coef1 : P) :=
> halfExtendedSubResultantGcd1(p,ts_v)$P
> | > | > | > d: P := hesrg.gcd; n: P := hesrg.coef1
> | > | > | > g := gcd(n,d)
> | > | > | > (n, d) := ((n exquo g)::P, (d exquo g)::P)
> | > | > | > remn, remd: Record(rnum:R,polnum:P,den:R)
> | > | > | > remn := remainder(n,ts); remd := remainder(d,ts)
> | > | > | > cn := remn.rnum; pn := remn.polnum; dn := remn.den
> | > | > | > cd := remd.rnum; pd := remd.polnum; dp := remd.den
> | > | > | > k: K := (cn / cd) * (dp / dn)
> | > | > | > pn := removeZero(pn,ts)
> | > | > | > pd := removeZero(pd,ts)
> | > | > | > [numer(k) * pn, denom(k) * pd]$Record(num:P, den:P)
> | > | > | > | > | | I belive that Axiom creators considered this function
> | > | > legal,
> | > | > | so generating error message would be a bug.
> | > | > Hmm, could you give me hints at to why they considered the function
> | > | > legal?
> | > | | Gaby, this case looks so simple. Rename hesrg in the "then"
> | > branch to
> | > | hesrg2 and to hesrg1 in the "else" branch.
> | > This *particular* case looks simple; I agree. However, I suspect my
> | > question is more about the *pattern* of the code. Said differently,
> | > is this type of code, something that should be valid? (Waldek says
> | > `no', and I tend to agree with him, but for different reasons).
> |
> I believe that the code could become legal with the same semantics if
> (a) branches of if-statements carry their own scopes; and
> (b) the declaration of `d' is moved just before the `if'.
The code can also be made legal by changing the definition of
halfExtendedSubResultantGcd1 and halfExtendedSubResultantGcd2 to return
something of type
Record (gcd: P, coef: P)
No "1" or "2" in the tag of the second field. *That* is an artificial
complication that is completely unnecessary.
> | Since
> | "if" does not introduce a new scope, the above code should be as
> | invalid as
> |
> | x: A := foo1()
> | x: B := foo2()
>
> Yes, that is what current Axiom compilers do.
>
> [...]
>
> | With "==" however, these lines in "main" are (according to the AUG)
> | equivalent to
> |
> | x(a: Integer): Boolean == foo1()(a);
> | x(a: Integer): Integer == foo2()(a);
> |
> | I think, you agree that this should be allowed.
>
> As it current is in all AXIOMs.
> These issues are orthogonal, I think.
What is orthogonal? That one forbids
x: A := foo1()
x: B := foo2()
but allows
x: A == foo1()
x: B == foo2()
if A is X->Y and B is U->V with (X,Y) not identical to (U,V)?
The problem is that the latter does not work properly in Axiom.
(1) -> foo1()(x:Integer):Integer == x
Type: Void
(2) -> x: Integer -> Integer == foo1()
Type: Void
(3) -> foo2()(x:Boolean):Boolean == x
Type: Void
(4) -> x: Boolean -> Boolean == foo2()
Type: Void
(5) -> x(true)
There are no library operations named x
Use HyperDoc Browse or issue
)what op x
to learn if there is any operation containing " x " in its name.
Cannot find a definition or applicable library operation named x
with argument type(s)
Boolean
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.
It looks like a bug, but I cannot exactly say why, because the meaning
of "==" in Axiom is not the same as in Aldor (I believe).
> | I have never felt a need for having an extra scope for if's.
>
> OK, but would you oppose others to have it?
How can I oppose. Open-Axiom is your project. You are the dictator. I
would not be in favour of new scopes, but if you must introduce an
incompatibility with old Axiom and Aldor then it is your choice and only
future will show whether people follow your decision or whether they
like the curren behaviour. I certainly only write library code for one
language. There is simply no time to make it work for all flavours of
Axiom. In fact, I would rather like that at least OpenAxiom and FriCAS join.
> | Branches should be short anyway
> Except when they are not -- as in almost every interesting algebra file.
"should be short"... the algebra stuff has to be revised anyway. This
sounds like you designing the language so that old code (that probably
will be thrown away or properly written in 5 years) works now.
Eventually one has to live with the modified SPAD forever.
> | and if one wants to have more computations inside the
> | "then" and "else", why not calling two functions there?
> Why would one _have_ to, if the computation is expressed in 2-3 lines?
Why not introducing a simple scope-creating syntax that is compatible
with existing syntax (and maybe even with Aldor)? I have no idea whether
other people would like that. I probably wouldn't even use that new
syntax, since code can already be nicely written without it.
> I prefer to have a language where the expression of the ideas match
> the conceptual meaning. If the variable is conceptually local, then I
> would like the language to support the expression of that idea.
So, if you must, make a variable implicitly local to branches of "if" if
it is not used outside the "if". Also that would make the above code
legal. And I think that would be a better way to express the conceptual
level. Of course, that can only work in SPAD. The interpreter has no way
to know whether or not a variable is used later so it should not be
local and have the same type in both branches.
> | As you have seen in my previous posting, this particular code can be
> | made without introducing any "local" variables, if the language is
> | strong enough (ie, with multivalues or Cross).
> For this _particular instance_ of the pattern, yes. But, what about
> the general pattern?
Could you show me an existing piece of Aldor or SPAD code, where there
is real need for local variables in branches? Or where it "feels
unnatural" if the code is rewritten to match current Aldor specification?
> In fact, except for the declaration of the local variable `d', I think
> the code was more readable without the manual mangling of the name --
> it gave same name to conceptually same thing, and the computations
> were 2-3 liners.
That's true, but as I said the problem is the type that is returned by
the halfExtendedSubResultantGcdn functions. So one should actually
rewrite that part of the library.
Ralf
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
