Sorry for being interfering, but I suppose there is some
misunderstanding which also puzzles me by now. IMO both of you are right
depending on the view. I believe that one point of confusion stems from
the intepretation of x:T as x \in T (which I also find attractive by the
way). However, FriCAS seems to have a different attitude to this:
(1) -> x:INT ; y:INT ; x+y
x is declared as being in Integer but has not been given a value.
(1) -> X:EXPR INT ; Y:EXPR INT ; X+Y
(1) X + Y
Type:Expression(Integer)
(2) -> U:EXPR COMPLEX INT ; V:EXPR COMPLEX INT ; U*V
(2) U V
Type:Expression(Complex(Integer))
Since INT is a ring one might expect to have z:=x+y evaluated of type
INT and if later setting x:=1, z evaluates to 1+y. This would be
consistent with the ring axioms. This is not the case even in EXPR INT:
(1) -> X:EXPR INT ; Y:EXPR INT ; Z:=X+Y
(1) Y + X
Type:Expression(Integer)
(2) -> X:=1::EXPR INT ; Z
(2) Y + X
Type:Expression(Integer)
(3) -> X
(3) 1
Type:Expression(Integer)
(4) -> ZZ:=X+Y
(4) Y + 1
Type:Expression(Integer)
Thus, although EXPR INT and EXPR COMPLEX INT behave in some way like R
and C respectively it is certainly inconsistent in the interpretation
mentioned at the beginning - from a logical point of view. I think that
the EXPR domain is merely a catchement basin to do symbolic
manipulations as many untyped CASs do. Coming to the point, I'm
speculating that there is some misconception between functions and
values on the one hand and between types and mathematical structures on
the other hand (see the sequence below).
(1) -> typeOf(sin)
(1) Variable(sin)
Type:
Type
(2) -> typeOf('sin)
(2) Variable(sin)
Type:
Type
(3) -> f:INT -> INT
Type:
Void
(4) -> typeOf(f)
(4) (Integer -> Integer)
Type:
Type
(5) -> typeOf(sin(x))
(5) Expression(Integer)
Type:
Type
That means (IMHO) an operation 'conjugate' or 'involution' or whatever
can only be defined in a satisfactory way if it's clear what is the
domain of definition and what is the range, thus z:C and f:C->C are not
only different types but also conceiving very different mathematical
structures. And here I slightly disagree with Bill:
> People try to do the opposite: They try to encode algebraic problems
> as logical ones (i.e. automatic theorem proving) but this has not lead
> to practical systems.
Logic is inherent, surely in many disguises (equational logic in algebra
for example), but how would you solve my initial problem (which
triggered my interest for this): given an equation x^2+y^2+z^2=1, get
FriCAS to provide an atlas automatically (polar coords excluded, no
magic ;). Clearly, one chart z(x,y)=sqrt(1-x^2-y^2) is easily
calculated, but how would you explain the domain of definition, openess
and so on without predicate logic? You might answer by dis/conjunction
of types as S.Thompson once proposed, however, that's logic too, even
HOL, and practically I'd be scared to compute an atlas of an algebraic
manifold by the help of type inference.
That's why I'm going to try an ATP (automatic theorem prover) in FriCAS,
called SNARK which might do the unpleasant inferences in the background.
By the way it's already (a little) working ...
https://bitbucket.org/kfp/snark.
Kurt
Am 05.12.2014 um 22:51 schrieb Bill Page:
> On 4 December 2014 at 08:08, Waldek Hebisch <hebi...@math.uni.wroc.pl> wrote:
>> Bill Page wrote:
>>>
>>> On 30 November 2014 at 20:58, Waldek Hebisch <hebi...@math.uni.wroc.pl>
>>> wrote:
>>>> Bill Page wrote:
>>>> ...
>>>> Depends on definition of 'conjugate'. One reasonable definition
>>>> of 'conjugate' on _functions_ is:
>>>>
>>>> conjugate(f)(z) = conjugate(f(conjugate(z)))
>>>>
>>>
>>> This looks odd to me. My understanding is that conjugate is not
>>> "functional" in the sense of acting on an entire function. When do
>>> we need such a "'conjugate' on _functions_"?
>
> I still wonder when we would need such a conjugate on functions? For
> example, why should we want to write
>
> conjugate(sin)(x)
>
> We already know that the 'sin' function is holomorphic (analytic), so
>
> conjugate(sin(x)) = sin(conjugate(x))
>
> for all x. Are you saying that this is somehow inconsistent with what you
> wrote
>
>>>
>>>> Basically the definition means that we compute 'conjugate' on
>>>> real axis and continue analytically to complex plane. This
>>>> definition is useful if we want to use 'conjugate' on complex
>>>> valued functions of real variable, but also want to use
>>>> analytic continuation.
>>>
>>> This also sense strange to me. I do not think of "computing
>>> 'conjugate on real axis". To me 'conjugate' is an algebraic concept,
>>> not a geometric one, so the concept of "real axis" does not apply.
>>> 'conjugate' however is a non-holomorphic (non-analytic) function.
>>>>
>>>> With such definition we have 'conjugate(z) = z' (here 'z' means
>>>> identity function!) and 'conjugate(sin(z)) = sin(z)'. But
>>>> this does not prevent the function to have complex values.
>>>>
>
> Maybe here would be a good place to discuss expressions versus
> functions. When you say: "here 'z' means identity function!" do you
> mean for example
>
> z(x) == x ?
>
> In which case z is obviously holomorphic and so what you wrote is true
> even if the notation is a bit odd (using equality of functions).
>
> For example, I would say that 'sin' is a function and 'sin(x)' is an
> expression with 'x' as a variable. So
>
> conjugate(z(x)) = z(conjugate(x))
>
>>>
>>> ??? Could you give a reference where 'conjugate' is defined in this
>>> way?
>>
>> There is a theory of Banach algebras with involution. The formula
>> I gave is standard definition of involution on Banach algebra
>> of holomorphic functions in a complex domain (of course the
>> domain must be invariant under 'conjugate'). If you are
>> interested Hoffman wrote a classic book, with title like
>> 'Banach spaces of analytic functions'. I do not remember
>> if the same symbol was used for conjugate on numbers and
>> operation on functions. Normally involution is denoted
>> by superscrit star ($f^*$), but conceptually involution
>> extend conjugate from a subalgebra of constant functions
>> to the whole algebra so using the same symbol falls within
>> accepted practice.
>>
>
> Certainly 'conjugate' is an involution. I suppose that what you
> proposing could be called an "involution algebra".
>
> http://www.encyclopediaofmath.org/index.php/Involution_algebra
>
> I have a copy of Hoffman's book but I do not see any explicit mention
> of involution.
>
>>>> More naively:
>>>>
>>>> (9) -> conjugate(z::Complex(Expression(Integer)))
>>>>
>>>> (9) z
>>>> Type:
>>>> Complex(Expression(Integer))
>>>>
>>>> Note: Complex is not a FunctionSpace, so directly no
>>>> contradiction is possible, but I hope that this example
>>>> illustrates that your change introduces an assumption
>>>> which is undocumented and hard to verify.
>>>>
>>>
>>> No I do not understand your illustration. With my patch I will get
>>> the result that you show above. But the construct
>>>
>>> Complex(Expression(Integer))
>>>
>>> also seems a little strange to me. There is nothing about "Expression
>>> Integer" that implies that it's elements are "real-valued",
>>
>> Exactly.
>>
>>> so this is like forcing a complex structure on top of something that
>>> already has (should have) one.
>>
>> No. Complex add solution of equation 'z^2 = -1'. If this equation
>> has no solution in base field, then Complex will produce nice
>> field. For example consider K = Q(sqrt(-3)). In K we can
>> solve 'z^2 = -3', but because 'sqrt(3)' is irrational we can
>> not solve 'z^2 = -1'. So Complex(K) is a field.
>
> OK.
>
>> In Expression(Integer) we have 'sqrt(-1)' so of course we are in
>> trouble if we really mean whole Expression(Integer).
>
> Yes, that was my point.
>
>> But usually we work with subfields and if in given subfield
>> 'z^2 = -1' is not solvable, then going to Complex makes sense.
>
> Do you mean that since we currently have no way to define explicit
> subfields (subdomains?) of Expression therefore we must admit this
> sort of abuse of Expression? What would be an example of such a
> sub-field? Do you mean something like "real-valued expressions"?
>
>> ...
>> Complex(Complex(Float)) is well defined, but is not a field,
>
> If 'Complex' was implemented as a as a Caley-Dickson construction
>
> http://axiom-wiki.newsynthesis.org/CaleyDickson
>
> then Complex(Complex(Float)) would be equivalent to the quaternions
> but unfortunately that is not what FriCAS/Axiom does right now.
>
>> so forming it leads to contradiction in assumption built into
>> algebra. Complex(Expression(Integer)) _may_ lead to
>> contradiction, but also has valid uses.
>>
>
> I admit that it might be useful but I still think it is a
> contradiction by definition.
>
>>
>> Well, product of two real numbers is real. Writing that in
>> terms of 'conjugate' leads to complicated expressions.
>
> I did not propose to write numbers in terms of 'conjugate' but rather
> real-valued expresses. The resulting expression is just a quadratic
> with 4 terms instead of one. To show that it is real-values is
> trivial.
>
>> For real numbers 'positive' is the same as being a square.
>> So you could try such an approach. But I have strong
>> reasons to believe that this will not work in practice.
>> First, you can encode logical problems into "algebraic"
>> setting, but this does not change nature of the problem.
>
> People try to do the opposite: They try to encode algebraic problems
> as logical ones (i.e. automatic theorem proving) but this has not lead
> to practical systems.
>
>> Why solving problem in unnatural setting should be better
>> then using natural one?
>
> Define "natural".
>
>> Second, once we enrich algebra to express notion of real
>> we hit unsolvability results of Richardson.
>
> Richardson showed that including both the positive branch of the
> 'sqrt' function and 'sin' as kernels in expressions formed by
> polynomials in one variable makes equality undecidable because it is
> equivalent to being able to show that an expression formed of just
> 'sin' and such polynomials is everywhere non-negative. So it may well
> be true that showing that a real expression of this kind can be
> written as a square is also undecidable. But it is not clear to me
> that simply introducing 'conjugate' and therefore being able to
> expression the notion of real results in the same thing.
>
>> OTOH many logical reasonings used in
>> practice are relatively simple. So working at logical
>> level (with conditions) naturally avoids unsolvability
>> (by refusing to solve hard prombles).
>
> That sounds like a contradiction to me.
>
>> In algebraic setting finding useful solvable class of
>> problems seems much harder.
>>
>
> What do you think are the obstacles to doing this?
>
> 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 fricas-devel+unsubscr...@googlegroups.com.
To post to this group, send email to fricas-devel@googlegroups.com.
Visit this group at http://groups.google.com/group/fricas-devel.
For more options, visit https://groups.google.com/d/optout.
