Andrew Miller wrote:
Hi all,
I have been looking into how we could define a typed lambda calculus
system in CellML, and have written up a document to collect ideas on this:
http://www.cellml.org/Members/miller/outline-of-a-typed-lambda-calculus-system
This document does not yet aim to be a formal specification, but
instead, aims to outline all the ideas that we could use as a basis for
writing up the relevant parts of the formal specification.
Please feel free to discuss this and / or suggest improvements. I have
enabled commenting on the document in Plone for people with an account,
and this mailing list would also be a suitable place for discussion of
the document to take place.
Of particular interest is ideas about how this could be applied, and of
anything that we could potentially be missing (for example, whether this
is sufficient to support stochastic simulations with the addition of a
few operators, or if it needs more fundamental changes to allow for
that. This is something I am still looking into and would welcome ideas on).
Hi Andrew (& all),
Overall I think this looks like a good approach, providing both
expressive power and elegance. The key difficulty will be in getting
the details right, both of semantics and XML encoding. This requires
concrete examples of how the concepts are envisaged to be used.
It would be good to have references to related work
(e.g. http://www.w3.org/TR/mathml-types/) and some comparison of the
pros and cons of each approach for CellML. To quote the MathML note,
"it is a well-known fact that developing a mathematical typing system
is a difficult task," so it would be beneficial to reuse existing work
if possible. I'd also like to know about existing /implementations/
using type systems with MathML - if we choose a sufficiently similar
system then this could help ease the implementation burden for
software authors.
One area I'd particular like examples for is the use of identifier
types. It would be good to be able to define 'a set of fluxes,' for
example, in a straightforward fashion, but I'm not sure what would be
the best way to do so. It's an interesting semantic question! In a
sense you want to be able to distinguish between 'a set of real
numbers with units of flux' (where you don't allow multiple members
with the same number value), and 'a set of variables of type
real_flux' (where variable identity, not value identity, is
considered). You then need to consider if the mathematical expression
"<apply><eq/><ci>x</ci><ci>y</ci></apply>" makes x & y identical
variables, or whether only connections achieve this. Perhaps a
multiset better captures this use case anyway, and the question is
moot?
Some other thoughts on various aspects of the proposal follow.
I was initially uneasy about lumping type and units information
together, since these are distinct concepts. I can see benefits, for
example the ability to link up type & units with a single connection.
We will certainly need a way to extract just the type or just the
units, however, and make sure that, say, an abstract 'squaring'
component can be defined (it would define a function from type T to
T^2, where T^2 has the same /type/ as T, but the units, if any, are
raised to the power 2).
I don't think it fits with the intended use of MathML to add items in
the CellML namespace directly to MathML elements (for example your use
of <cellml:function_type />). This requires validators to alter the
MathML schema they use. An alternative approach would be to make use
of the facilities MathML already provides, such as csymbol and the
type attribute (using the latter on cn elements would allow use of
cellml:units to be deprecated).
One approach to defining functions of multiple arguments is given in
http://www.w3.org/TR/mathml-types/.
Do we need to define an explicit 'struct' equivalent? Could we not
use cartesian products (which are already in MathML)? This provides
us with arbitrary tuple types - the only difference from a C struct is
that you can't name members.
_______________________________________________
cellml-discussion mailing list
cellml-discussion@cellml.org
http://www.cellml.org/mailman/listinfo/cellml-discussion
