First login?
Lost password?
 
 
cellml-discussion AT lists.cellml.org 
CellML Discussion List

Text archives Help


[cellml-discussion] A typed lambda calculus system for CellML


Chronological Thread 
  • From: ak.miller at auckland.ac.nz (Andrew Miller)
  • Subject: [cellml-discussion] A typed lambda calculus system for CellML
  • Date: Wed, 06 Aug 2008 11:55:31 +1200
Alan Garny wrote:
> Hi Andrew,
>
>
>> 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 is a good starting point, well done!
>
>
>> 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).
>
> Regarding stochastic models and based on your current document, I am
> wondering whether it wouldn't be worth having/gathering (snippets of) models
> that would ideally be described in a typed CellML format?
>
> I don't know anything about stochastic modelling, but if we were to have
> such (snippets of) models, it might help us determining what is required to
> get "a typed lambda calculus system [(TLCS)] could work in CellML".
>
> Anyway, back to your document (please keep in mind that I haven't really
> thought about TLCS):
>
> Variables as types:
> -------------------
> - Do we really want to allow generic types? I am concerned that this could
> lead to models that are not bullet-proof.
>
The core of CellML can be very generic, and then secondary
specifications can narrow down CellML to a subset of CellML which can be
implemented by a particular tool. Models would then be coded up in
accordance with a secondary specification.

One secondary specification would likely only allow real numbers, and
other parts of the secondary specification might also allow the use of,
say, vectors of real numbers. But the core specification has to be more
general so that more secondary specifications can be defined.

> - "In order to provide built-in types, there will need to be built-in
> variables." I think I understand the concept of "built-in types", but I am
> not sure what you mean by "built-in variables". Could you please provide us
> with some concrete examples of those?
>
Remember that the core statement of how the TLCS works is that "CellML
variables are defined inside components to hold types". In other words,
types are stored in variables. If we want to have built-in types, we
need to have variables to store them in, hence built-in variables. I
think that perhaps I need to emphasise the idea of variables holding
types more somehow.

real_metre is an example of a built-in variable, which is given in the
same paragraph.

> - "It would be valid to connect a built-in type using the name of one
> component to another variable". I must confess that this doesn't really make
> sense to me. I think it would help if you were to give some concrete example
> (the example you give in your document is still somewhat abstract).
>
I could add in something like:
Component A:
Variable name="T" type="type"
* Some more variables of type T *
Maths in terms of variables of type T

Component B:
Empty

Connection
Between Component A and Component B
Connect Component A.T to Component B.real_metre

This would cause all the variables in Component A to be in terms of
real_metre. This is valid.

> - "However, it would be invalid to connect two built-in variables to each
> other." I guess I will understand that statement once I know exactly what a
> "built-in variable" 'looks like'.
>
For example, the following would be invalid...
Component A:
Empty

Component B:
Empty

Connection
Between Component A and Component B
Connect Component A.real_metre to Component B.real_second

Here, real_metre and real_second are both built-in variables.

> - You mention "real_metre" as an example of a built-in variable. For some
> reason, I would have thought of "real_metre" as being an example of built-in
> type...
Because all types are stored in variables. So real_metre is a built-in
variable of type "type".
> Why would all components have a built-in variable called
> "real_metre"?
Because real_metre is 'superglobal' meaning that it is automatically
present in all components, saving the need to connect it up and
simplifying the common case.

> What used would such a variable have?
So that type="real_metre" can be used on a variable... in which case,
the variable real_metre would be searched for, and since it is present
in every component, found. This is explained in the third paragraph of
"variables as types".

> On the other hand, I
> could see the need for such a type to be available everywhere. I have the
> feeling that this might be a matter of terminology?
> - Variables as types: "Variables holding a type have type "type", where type
> is a built-in variable which itself has type "type"." Could this be
> rephrased?!
>
I don't think we can avoid using the word type so many times, and IMHO
it would be even more confusing to mix different words meaning type.
Dealing with the type of types is important.

> MathML operators for dealing with types:
> ----------------------------------------
> - "Creating types which represent the product space of two (or more) other
> types. For example, given the types real_metre and real_second, creates the
> type for both a real_metre and real_second." Couldn't you refer to "product"
> rather than "product space"?
I mean product space in the sense that the set of acceptable values for
the type is the cartesian product of the sets of possible values of the
types the operator is applied to. So for example, a variable of the
product space type of real_metre x real_second could take the value (5m,
10s).

> Otherwise, to illustrate the product of
> real_metre and real_second, couldn't you say that you end up with something
> like real_metre_second, or am I missing something?
>
No, that is a different operator, the one described as "making a new
real number type to represent the dimensions of a product of two
existing real number dimensions".

> - "Creating the type of a function in terms of the return type and the
> argument types." Could you please give a concrete example of what you mean
> by this?
>
See the functions section further down in the document.

> - "Reversing the operations of the previous two operators". I first need to
> understand those two operators to know whether I understand/agree with that
> statement.
>
> Dealing with real numbers:
> --------------------------
> - "The equivalence rules would enforce dimensional consistency, but
> automatically apply conversion factors." Did you really mean that or "the
> equivalence rules would *NOT* enforce dimensional consistency, but
> automatically apply conversion factors", or even something else?
>
Sorry, that was a mistake. It should read something like:

"The equivalence rules would enforce dimensional consistency, and
conversion factors would be automatically applied at connections. There
would be no automatic insertion of conversion factors in dimensionally
consistent but units inconsistent equations."

> - "An operator which relates a real type A to two real types A and B such
> that..." I suppose you meant "An operator which relates a real type *X* to
> two real types A and B such that..."?
>
Indeed.

> - You may, for the last three operators, want to swap A and X, so that it is
> consistent with the first operator (e.g. for the second operator, it should
> read "An operator which relates a real type X to a real type A and...").
>
True.
> - Paragraph starting "The specification would define that two types are
> equivalent if...": though I do understand what you are saying, it might help
> some people to give a concrete example.
>
See the next sentence in that paragraph, which gives an example.

> - "Identifier types are the exception, and can be used to provide semantics
> like 'tag types' in other languages when this is required." This is lost on
> me. Note: I see that "identifier types" are 'defined' in the next section.
>
> Identifier types:
> -----------------
> - It would help if you could give some examples of identifier types.
>
See the two bullet points at the end of the section on identifier types.
> - "Secondly, we *NEED* new context-sensitive MathML constructors for..."?
>
That is indeed what I intended to write.

> - I need to understand what is exactly meant by "Identifier types" before
> being able to feed back on this section.
>
The idea is a type, the values of which serve no purpose other than to
be unique. Having uniqueness available to modellers allows constructs
which attribute meaning to equality, such as set membership, to be given
the correct semantics. For example, if different parts of the model
indicate that fluxes belong to the set of all fluxes acting on a
species' concentration, the desired interpretation is that each flux
belongs to the set once per part of the model which adds the flux, not
once per unique numerical value of the flux (if another part of the
model sums over the values of the set to get the rate, and there are two
separate reactions which generate numerically identical fluxes, both of
these fluxes should be added to get the rate). In this case, it is
useful to 'tag' the values being added to the set with an identifier, so
that they are compared for the purposes of the uniqueness of set members
based on the identifier and not the value.

> Functions:
> ----------
> - I am not clear why the variable "fn_seconds_to_metre" is of type "type".
>
fn_seconds_to_metre is the type of a function which takes a single
parameter in seconds, and returns a value in metre. Since the variable
holds a type, it has a type="type" attribute.

> You mention something about type "type" in the last paragraph of the
> "Variables as types" section. Is that related?
>
Yes, this variable has the predefined type "type".

> - I agree that functions that take one or more parameters is the best
> approach.
> - You might want to provide some concrete examples of the advantages you
> list. I am, for example, not clear what you mean by the third advantage that
> you listed.
>
Yes, this is something that still needs to be done... ideally we should
build some examples of complete models, including those using time
delays and summary statistics, coded up according to the draft versions
of CellML 1.2.

I mean that it makes more sense to say:
<apply>
<diff/>
<bvar><ci>time</ci></bvar>
<apply><ci>x</ci>
<ci>time</ci>
</apply>
</apply>

than to say:
<apply>
<diff/>
<bvar><ci>time</ci></bvar>
<ci>x</ci>
</apply>

because otherwise x is sometimes taken to mean the value at a particular
point in time, and other times, has a calculus operator applied to it
treating it as a function of time.

> Structured types:
> -----------------
> - "However, for these types, it most likely would be reasonable that all
> members are of the type would be of the same type, and so we should specify
> the element type for all members." This is not clear to me. Are you saying
> that for each member of, say, a vector, we should specify its type? I.e. we
> could have a vector V[3] with V[0] = 123 {integer}, V[1] = true {boolean}
> and V[2] = 456.789 {float}.
>
No, I meant a single element type for all members.
> - You might want to give a concrete example of structured type.
> - "Another useful type to have would be a structured type *WITH* differently
> typed elements..."?
>
It was probably going to be "which has", but with is just as good.
> - "Extracting the sizes / dimensions of vector / matrix / set / list types."
> Could you please give a concrete example of this?
>
I guess a more complete example model would be a good place for this...
this would be particularly useful for highly reusable components which
don't have full details a priori about what they are going to be
connected up to.

> Miscellaneous:
> --------------
> - As a general rule, I would very much welcome concrete examples and a not
> so abstract/formal style of writing (unlike for the specifications). If find
> the current version of your document to be unnecessarily difficult to read.
> If you want feedback (and I want you to get some!), you would, in my
> opinion, greatly benefit from writing in a much simpler style. Remember that
> we are not all native English speakers and haven't all put loads of thoughts
> in TLCS... This being all said: well done indeed!
>

Thank you for your feedback, I am finding it very helpful, and at some
point I will probably do a second iteration to try to take these into
account (I don't want to change the document under people who might be
reviewing it just yet).

Best regards,
Andrew

> Alan
>
> _______________________________________________
> cellml-discussion mailing list
> cellml-discussion at cellml.org
> http://www.cellml.org/mailman/listinfo/cellml-discussion
>



Archive powered by MHonArc 2.6.18.

Top of page