[Axiom-developer] [Tuples Products And Records]

[Bill Page]

Changes 
http://page.axiom-developer.org/zope/mathaction/TuplesProductsAndRecords/diff
--
William Sit wrote:

> 'Product(A,B)' is not the same as '(A,B)' computationally, as it is
> currently in Axiom.

Yes, I agree that is true in Axiom as it is now. But I am thinking about
how Axiom should be not how it is. The mathematical concept of product
is straight-forward and there is no reason why '(A,B)' where 'A' and
'B' are domains should not denote this product.

The derived domain Product, as it is defined now in Axiom is rather
more complicated than what one needs for defining a Mapping for
a function with more than one input. The domain Tuple on the other
hand is too restricted. Axiom's built-in primitive domain Record
is just about right.

> So currying is nothing but specialization ...

No, specialization is not equivalent to currying. The result of
currying is a higher-order function. Specialization is applying
that function to a specific argument. See for example:

http://en.wikipedia.org/wiki/Currying

Unfortunating the funtions called curryLeft and curryRight are
actually specializations:
\begin{axiom}
)di op curryLeft
)di op curryRight
\end{axiom}

What we need is a function
\begin{axiom}
leftCurry:((INT,INT)->INT)->(INT->(INT->INT))
leftCurry(f)== x+->(y+->f(x,y))
\end{axiom}

But the Axiom interpreter is not able compile this function.

See [Sandbox Curry] for more attempts to define this in Axiom.

> using a computer. We can't really do "symbolic computation"
> the way a human mind can.

I do not know anything of an algorithmic nature that a human mind
does which cannot in principle be done on computer. As I understand
it dealing with " ... (ellipsis)" is one of the purposes of the
construct called Streams in Axiom.

> You did not answer my question on arity.

Do you mean the question of the arity of, for example the following
function::

  f:Product(A,Product(B,C))->D

My answer (assuming that you accept the notion of Product as a
primitive domain) would be that this function has "arity" of 3
since in a Cartesian closed category (CCC) we have

  Product(A,Product(B,C)) = Product(Product(A,B),C) = Product(A,B,C)

Axiom actually takes the domain Record as primitive rather than
Product. The equivalence of constructs such as::

  Record(a:A,b:Record(a:B,b:C)) = Record(a:Record(a:A,b:B),b:C) =
  Record(a:A,b:B,c:C)

is a little less obvious but natural coercions (isomorphisms) could
be provided which make the question of arity clear in this case as
well.

> The design of the domain Product(A,B) need not be dominated by the
> two projection maps.

That is not true. The very nature of what we mean by product is
defined in terms of these projection maps. The product is what is
known as a type of limit in category theory. It is defined by a
universal property which makes the product and it's projection
maps unique amoung all other such objects and maps. See for
example:

http://en.wikipedia.org/wiki/Limit_(category_theory)

> Consider the two ways of coding ... f, g

Using the Record constructor in Axiom this function can be
written as:
\begin{axiom}
h:Record(a:INT,b:INT)->INT
h(parameter) == parameter.a + parameter.b
h[1,2]
\end{axiom}

which is almost as convenient as your definition of 'g'. Syntactically,
the name 'parameter' could be eliminated for brevity. There is no
reason that the compiler should produce less efficient code for this
notation.

> Is CCC the only kind of categories in symbolic computation?

That is a long story that I plan to continue here
[Cartesian Closed Category]. But very briefly one answer to
your question could be: CCC is the smallest and simplist kind
of category in which we should expect to be able to do all the
symbolic computation that is possible on a computer. The reason
why we can say this with some certainty has to do with the
relation between CCC and the simple-typed lambda calculus.

Lambda calculus is the smallest and simplist programming language
which can be shown to be computation universal, i.e. in which we
can prove that it is possible to express all computable functions,
the partial recursive functions or equivalently to simulate a
Turing machine.

(Cf. previous reference to CCC for all this "jargon" :)
--
forwarded from http://page.axiom-developer.org/zope/mathaction/address@hidden