From 9b40745aabb9a53971f8734ac303b85dfa9ce533 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Fri, 13 Aug 2021 16:02:17 +0200 Subject: [PATCH 01/11] Add proposed language specification. Just the first more or less complete draft! --- doc/specification/language-proposal.md | 1518 ++++++++++++++++++++++++ 1 file changed, 1518 insertions(+) create mode 100644 doc/specification/language-proposal.md diff --git a/doc/specification/language-proposal.md b/doc/specification/language-proposal.md new file mode 100644 index 0000000..8b61a10 --- /dev/null +++ b/doc/specification/language-proposal.md @@ -0,0 +1,1518 @@ +# Arblang proposal + +Arblang is a language for defining the dynamics and effects of Arbor 'mechanisms'. A mechanism is a stateful process whose evolution over time is governed by a system of ODEs and by responses to external events, and which in turn acts upon the cellular state to which the mechanism is applied. + +The Arblang language is constrained so that every evolution and effect can be interpreted _symbolically_ as closed form expressions. This is to permit the automatic analysis of these expressions for the purposes of determining a priori analytic solutions or appropriate ODE approximation techniques, and to automatically determine, for example, time derivatives of effect values through symbolic or automatic differentiation. Consequently common programming constructs such as unbounded iteration or recursion are precluded. + +Arblang nonetheless can also be interpreted in a purely numerical fashion in other contexts. + + +# Mechanism semantics + + +A mechanism can be one of a number of different _classes_ of mechanism, where each class determines the sort of cell interactions that the mechanism performs. The classes are pre-defined, but are open ended, in that further extensions to Arbor may admit new mechanism classes. The basic set of classes are described as follows: + +* _Density mechanisms_ describe processes with spatial extent, and their effects are described in terms of current densities and molar fluxes of ionic and nonionic species. They do not receive events. + +* _Concentration models_ determine the evolution of internal or external species concentration over some spatial extent, based upon the species fluxes and other cellular state. They also do not receive events. + +* _Point mechanisms_ describe localized processes, with effects defined in terms of currents and molar flow rates. They can change their state in response to spikes from other cells from connections that are bound to them, or to spikes generated by the cell on which they are placed. + +Each of these mechanisms can have a _state_ comprising zero or more named values that vary over time. Each mechanism definition will provide the initial values for this state, and define their evolution by an explicit system of ODEs. + + +## External bindings + + +The definition of a mechanism allows for names to be bound to the mechanism state and various cellular quantities so that they can play a role in defining the evolution and effects of the mechanism. + +The list of possible cellular quantities is open to future extension, but initially are as follows: + +* _State_ refers to the evolving state of the mechanism itself. + +* _Membrane potential_ is the potential difference across the cellular membrane. + +* _Temperature_ is the local temperature at the cellular membrane. + +* _Molar flux_ is the local transmembrane flux associated with an ionic or nonionic species. + +* _Current density_ is the local transmembrane current associated with an ionic species. This is related to the species molar flux by the ionic charge and the Faraday constant. + +* _Charge_ is the fixed electrical charge of an ionic species, given as a dimensionless multiple of the elementary charge. + +* _Internal concentration_ and _external concentration_ are the intracellular and extracellular concentrations respectively of a species, in the vicinity of the cellular membrane. + +Not every mechanism class has access to every cellular quantity. In particular, only concentration models have access to current densities and molar fluxes. + + +## Effects + + +Effects define how the mechanism state influences the cellular state. The list of possible effects is open to future extension, but the initial effects are as follows: + +* _Current_ defines an ionic current contribution or non-specific current contribution (one not explicitly associated with any ionic species) to the transmembrane currents by a localized process. + +* _Current density_ defines similarly a contribution to the ionic or non-specific transmembrane current densities by a process with spatial extent. + +* _Molar flow rate_ defines a contribution to the transmembrane flow of a species by a localized process. + +* _Molar flux_ defines a contribution the transmembrane flux of a species by a process with spatial extent. + +* _Internal concentration rate_ and _External concentration rate_ define the contribution to the rate of change in the intracellular or extracellular concentrations respectively of a given species. + +A mechanism can define an effect in terms of an ionic current (or current density) or in terms of a species flow (or flux), but not both. A current defines an ionic flow, and vice versa. + +Restrictions: + +* Concentration models can only have concentration effects. + +* Point mechanisms can only have current or molar flow rate effects. + +* Density mechanisms can only have current density or molar flux effects. + + +## Events + + +As noted above, point mechanisms can receive _events_, upon which their state can be modified according to some formula. There are currently two supported sorts of events: + +* _Event_ is triggered when by a spike on an attached connection. It has a scalar value equal to the connection weight. + +* _Post_ is triggered when a spike is generated on the post-synaptic cell. There may be a delay between the spike generation and the _post_ event; the value of the _post_ event is the time between the spike generation and the event delivery. + + +## Parameters + + +A mechanism can include _parameters_. These are named quantities with a default value that are constant throughout the evolution of a mechanism's state, but which can be overridden with user-supplied values when the mechanism is used in a cell model. + +For a parameter to be settable, it must be explicitly exported in the mechanism definition. + + +## Regimes + + +The dynamics of the mechanism are governed by one or more dynamical _regimes_. Within a regime, the evolution of the mechanism state is provided via an explicit ODE system, and predicates on that state or external events can trigger discrete changes in the state value and a state transition to a different regime. + + +# Lexical grammar + + +Tokenization is governed by a grammar, described below in a variant of BNF, with the notation: + +* Names for non-terminals are written in _italics_ and may not contain spaces. + +* Non-terminals that constitute tokens are written in ***bold-italics***. + +* Terminals are written in `monospace`, denoting the exact character sequence thus represented. + +* A terminal may also be written as a Unicode code point, as 'U+' followed by four or five hexadecimal digits followed optionally by the literal character and then optionally by the Unicode name in all capitals. + +* A set of single character terminals can be denoted by {expr} where _expr_ is a one- or two-letter Unicode general category abbreviation, indicating the corresponding collection of characters, or a binary Unicode property, indicating the collection of characters for which the property has the value 'Yes'. + +* A set of single character terminals can also be denoted by a character class […] following the syntax described in [Unicode Regular Expressions](https://www.unicode.org/reports/tr18) sections 0.1.1, 1.2.4, and 1.3. + +* Symbols can be grouped with parentheses. + +* Alternatives are delimited by a vertical bar |. + +* An asterisk indicates the preceding symbol or group is repeated zero or more times. + +* A plus sign indicates the preceding symbol or group is repeated one or more times. + +* A question mark indicates the preceding symbol or group may be omitted, that is, it can appear at most one time. + + +## Character set + + +Arblang source is represented as a sequence of Unicode characters in normalization form C (NFC), excluding unassigned characters, surrogate code points, non-characters, and byte order marks. It is the responsibility of the interpreting environment to transform any particular source encoding to this representation. + + +## Tokenization + + +A lexically valid Arblang source must admit a tokenization as a sequence of ***comment*** tokens, ***whitespace*** tokens, ***symbol*** tokens, ***string-literal*** tokens, ***superscript-literal*** tokens, ***numeric-literal*** tokens, and punctuation tokens. + +A token has an associated value, which may be empty. If not empty, it is the result of applying a token-specific canonicalization process. +With the exception of string literals, canonicalization first applies Unicode compatibility normalization NFKC to the token text, then further processing as detailed below. + + +### Comments + + +A comment is introduced by `#` and then extends to the end of the line. It is the only context in which a line end is not regarded simply as whitespace. + +> ***comment*** ::= U+0023 `#` NUMBER SIGN _comment-character_* _new-line_ +> +> _comment_character_ ::= [^\\u{000A}\\u{000B}\\u{000C}\\u{000D}\\u{0085}\\u{2028}\\u{2029}] +> +> _new-line_ ::= _cr_ | _lf_ | _cr_ _lf_ | _other-newline_ +> +> _lf_ ::= U+000A LINE FEED +> +> _cr_ ::= U+000D CARRIAGE RETURN +> +> _other-new-line_ ::= U+0085 NEXT LINE | U+2028 LINE SEPARATOR | U+2029 PARAGRAPH SEPARATOR + +#### Token value + +A ***comment*** token has no value. + +#### Notes + +A _comment-character_ is any character that is not the first character of _new-line_. New line characters and sequences correspond to the [line boundaries requirement RL1.6 of Unicode Regular Expressions](https://www.unicode.org/reports/tr18/#RL1.6). + + +### Whitespace + + +In some expressions, where it denotes multiplication, whitespace is mandatory, but otherwise whitespace is not significant. It comprises any non-empty sequence of characters with the White_Space property. + +> ***whitespace*** ::= {White_Space}\+ + +#### Token value + +A ***whitespace*** token has no value. + + +### Symbols + + +Symbols correspond to Arblang identifiers and keywords. Arblang keywords are generally contextual: the interpretation of a symbol as an identifier or a keyword is determined in parsing. + +> ***symbol*** ::= _symbol-start_ _symbol-continue_\* | _symbol-degree-prefixed_ +> +> _symbol-start_ ::= {L} | {Nl} | {Other_ID_Start} +> +> _symbol-continue_ ::= _symbol-start_ | {Nd} | {Mn} | {Mc} | {Pc} | _prime-mark_ +> +> _prime-mark_ ::= U+0027 `'` APOSTROPHE | U+02B9 `ʹ` MODIFIER LETTER PRIME | U+2032 `′` PRIME +> +> _symbol-degree-prefixed_ ::= U+00B0 `°` DEGREE SIGN {L}+ | U+2109 `℉` DEGREE FAHRENHEIT | U+2109 `℃` DEGREE CENTIGRADE + +#### Token value + +Canonicalization substitutes any character in _prime-mark_ with U+0027 APOSTROPHE after performing NFKC normalization. + +#### Notes + +Identifiers broadly follow the conventions of Python, except: +* `_` is not a valid _symbol-start_. +* A ***symbol*** may contain _prime-mark_ characters. +* Special degree-sign prefixed symbols are permitted, in order to represent temperature scales. Compatibility characters U+2109 `℉` and U+2109 `℃` will be converted to `°F` and `°C` respectively in NFKC normalization. +* Characters that are only _compatibility_ equivalent to an acceptable _symbol_ character are not permitted. In particular, superscript numerals are not permitted within a _symbol_. + + +### Superscript literals + + +A superscript literal is used to denote exponents in the absence of the exponentiation operator. + +> ***superscript-literal*** ::= _superscript-minus_? _superscript-digit_+ +> +> _superscript-minus_ ::= U+207B `⁻` SUPERSCRIPT MINUS +> +> _superscript-digit_ ::= `⁰` | `¹` | `²` | `³` | `⁴` | `⁵` | `⁶` | `⁷` | `⁸` | `⁹` + +#### Token value + +After NFKC normalization, which takes superscript digits and minus to regular digits and U+2212 MINUS SIGN, the token value is canonicalized by mapping U+2212 to U+002d `-` HYPHEN-MINUS. + + +### Numeric literals + + +Numeric literals represent both fractional and integer literal values. + +> ***numeric-literal*** ::= _digit-sequence_ (_decimal-separator_ _digit-sequence_)? _exponent_? +> +> _digit-sequence_ ::= ( `0` | `1` | `2` | `3` | `4` | `5` | `6` | `7` | `8` | `9` )+ ( _digit-group-separator_ _digit_sequence_)? +> +> _digit-group-separator_ ::= U+0027 `'` APOSTROPHE | _whitespace_ +> +> _decimal-separator_ ::= U+002E `.` FULL STOP +> +> _exponent_ ::= _exponent-E_ | _exponent-alternate_ +> +> _exponent-E_ ::= ( 'E' | 'e' ) _sign_? _digit-sequence_ +> +> _exponent-alternate_ ::= U+00D7 `×` MULTIPLICATION SIGN _whitespace_? `10` _superscript-literal_ +> +> _sign_ ::= U+002B `+` PLUS SIGN | U+002D `-` HYPHEN-MINUS | U+2212 `−`MINUS SIGN + +#### Token value + +After normalization, which takes superscript digits and minus to regular digits and U+2212 MINUS SIGN, the token value is canonicalized as follows. +* Any _digit-group-separator_ is removed (including all whitespace). +* U+2212 MINUS SIGN is mapped to U+002D `-` HYPHEN-MINUS. +* U+002B PLUS SIGN is removed. +* Exponential markers `e` and `×10` are replaced with `E`. + +#### Notes + +* The use of whitespace as a digit group separator is intended to accommodate SI practice of writing long numbers, e.g. `10 000 000` for 10⁶. +* The alternate scientific number syntax `1.234 45 × 10³` is allowed in order to support standard SI practice. `×` is not used elsewhere as an arithmetic operator. +* The apostrophe digit separator is also used in C++14 for integer literals. +* Though a space preceding an 'E'-style exponent does accord to some typographic conventions, a space is not permitted in this syntax so that reaction complexes such as `2 E + 4 A` do not get tokenized as a numeric-literal `2E4` followed by a symbol `A`. +* In order to accommodate loss-free rescaling of unit-bearing quantities, real and integer literals in arithmetic contexts should have an internal representation that maintains a normalized significand and a power of ten scale. + + +### String literals + + +String literals encode arbitrary character sequences used to specify and identify interface and species names. + +> ***string-literal*** ::= `"` ( [^\"]* | _escape-sequence_ )\* `"` +> +> _escape-sequence_ ::= `\\` | `\"` + +#### Token value + +The value is taken as the characters between the initial and final `"` characters, followed by the replacement of each _escape-sequence_: `\\` by `\` and `\"` by `"`. + +#### Notes + +The value of a ***string-literal*** token does _not_ undergo NFKC normalization, and so comprises an arbitrary sequence of Unicode characters in NFC normalization. While the syntax allows arbitary white space within a literal, including line separators and similar, the interpreting environment might impose further restrictions on what constitutes a valid interface name, for example. + + +### Punctuation + + +> _punctuation_ ::= +> ***plus-sign*** | ***minus-sign*** | ***multiplication-dot*** | ***division-slash*** | ***exponent-op*** | ***preferential-union*** | +> ***compare-equal*** | ***compare-not-equal*** | ***compare-less*** | ***compare-less-equal*** | ***compare-greater*** | ***compare-greater-equal*** | +> ***left-arrow*** | ***right-arrow*** | ***right-left-arrow*** | ***empty-set*** | ***square-root*** | +> ***assign-equal*** | ***semicolon*** | ***left-paren*** | ***right-paren*** | ***left-brace*** | ***right-brace*** | +> ***colon*** | ***bar*** | ***comma*** | ***period*** + +Punctuation token definitions: + +> ***plus-sign*** ::= `+` +> +> ***minus-sign*** ::= U+002D `-` HYPHEN-MINUS | U+2212 `−`MINUS SIGN +> +> ***multiplication-dot*** ::= U+00B7 `·` MIDDLE DOT | U+22C5 `⋅` DOT OPERATOR +> +> ***asterisk*** ::= `*` +> +> ***division-slash*** ::= U+002F `/` SOLIDUS | U+2215 `∕` DIVISION SLASH +> +> ***exponent-op*** ::= `^` +> +> ***preferential-union*** ::= `&` | U+2294 `⊔` SQUARE CAP +> +> ***compare-equal*** ::= `==` +> +> ***compare-not-equal*** ::= `!=` | U+2260 `≠` NOT EQUAL TO +> +> ***compare-less*** ::= `<` +> +> ***compare-less-equal*** ::= `<=` | U+2264 `≤` LESS-THAN OR EQUAL TO +> +> ***compare-greater*** ::= `>` +> +> ***compare-greater-equal*** ::= `>=` | U+2265 `≥` GREATER-THAN OR EQUAL TO +> +> ***left-arrow*** ::= `<-` | U+2190 `←` LEFTWARDS ARROW +> +> ***right-arrow*** ::= `->` | U+2192 `→` RIGHTWARDS ARROW +> +> ***right-left-arrow*** ::= `<->` | U+21C4 `⇄` RIGHT ARROW OVER LEFT ARROW +> +> ***empty-set*** ::= `\0` | U+2205 `∅` EMPTY SET +> +> ***square-root*** ::= U+221A `√` SQUARE ROOT +> +> ***assign-equal*** ::= `=` +> +> ***semicolon*** ::= `;` +> +> ***left-paren*** ::= `(` +> +> ***right-paren*** ::= `)` +> +> ***left-brace*** ::= `{` +> +> ***right-brace*** ::= `}` +> +> ***colon*** ::= `:` +> +> ***bar*** ::= U+007C `|` VERTICAL LINE +> +> ***comma*** ::= `,` +> +> ***period*** ::= `.` + +#### Token value + +Punctuation tokens have no value. + + +# Arblang syntax and semantics + + +The syntax definitions below are defined in terms of the tokens defined in the lexical grammar, with the following conventions: + +* A ***symbol*** token can represent an identifier or a keyword; keywords in the syntax descriptions are written in `monospace`, and should be interpreted as ***symbol*** tokens with the corresponding value. + +* Where ***whitespace*** is present in a syntax rule, it is required, but additional ***whitespace*** tokens are permitted anywhere in the (tokenized) Arblang source, where they are ignored. + +* For readability in syntax rules, the text representation of a punctuation token, styled monospace, may stand in for the punctuation token itself. So, for example, `=` might stand for the token ***assign-equal***. + +An Arblang source document comprises a series of module and interface definitions. + +> _source_ ::= ( _module-defn_ | _interface-defn_ )+ + +Module and interface definitions are described below. + +## Identifiers and scope + + +Identifiers are represented by ***symbol*** tokens and depending on context, may refer to: +1. a module, +2. an imported module, +3. a constant, +4. a parameter, +5. a function, +6. an external binding, +7. a type alias, +8. a regime, +9. a record field, +10. a function argument, +11. or a local value binding. + +### Scopes + + +The association of an identifier with its referent is called a _binding_, and that binding is valid only within a _scope_. With one exception for regime names, an identifier's scope does not precede the point where that identifier is introduced by some declaration or binding. + +**Global scope.** +A module definition introduces the module name into the following global scope. The environment may also introduce module names defined in other Arblang sources. + +**Module scope.** +Within a module or interface definition, top-level parameter, constant, type alias, and function definitions have module scope, as do module imports and external bindings. The scope extends from after the definition or import, until the end of the enclosing module or interface. Identifiers bound in module scope can be made visible in other modules as a _qualified-identifier_ after a module import. + +**Function scope.** +Function arguments have function scope, which extends until the end of the function definition. + +**Regime scope.** +All top-level regime definitions in an interface have as scope the entire interface definition, even preceding the regime definition. The same applies within a region definition: the scope of an internal region identifier is the entire body of the region definition. An internal region identifier is visible as a _qualified-identifier_ elsewhere within the same interface definition. + +**Expression scope.** +`let` and `with` binding expressions introduce new identifiers that have as scope the final expression in the binding. + +**Record scope.** +Field names introduced in a record type or record value have record scope, which extends to the end of the record type or record value construction. + +Scope form a hierarchy of inner and outer scopes, with the outermost scope being the global scope. + +### Context + + +Two different identifiers with the same ***symbol*** may be bound in the same scope, if they are in different _contexts_. There are five distinct contexts in Arblang: + +1. _Module_ context applies wherever a module name is being introduced in a module definition, or where a module is referenced in a module import clause. +2. _Type context_ applies in type expressions and where a type alias is introduced. +3. _Regime context_ applies in regime clauses and where a regime name is introduced in a regime definition. +4. _Record context_ applies to field names within a record type description or in a record value construction. +5. _Expression context_ applies within value expressions, function argument definitions, the definition of parameters, constants, functions, and in the association of an identifier with an imported module. + +Each context can be regarded as constituting a different namespace for identifiers. + +### Masking + + +An identifier bound in a given context in an outer scope may be _masked_ by a binding of an identifier with the same ***symbol*** in an inner scope. This is permitted only in the following circumstances: + +1. An identifier bound in expression context in a function scope by a function argument or in expression scope by a `let` or `with` binding may mask an identifier in an outer scope. +2. An identifier bound in regime context in an inner regime definition may mask a regime identifier in an outer regime or interface scope. + +It is otherwise an error to bind an identifier with the same ***symbol*** as an already bound identifier in the same context. + +### Qualified identifiers + + +A qualified identifier is a term of the form: + +> _qualified-identifier_ ::= ***symbol*** ( `.` ***symbol*** )\* + +A qualified identifier of the form α._id_, where α is a (qualified) identifier and _id_ is an identifier, is bound to the referent of _id_ in the scope determined by α: + +1. In an expression context, if α is bound to a record value, then α._id_ is bound to the value of the field named _id_ in α. +3. In an expression context, if α is bound to an imported module, then α._id_ is bound to the constant, parameter, or function bound to _id_ in the module referred to by α. +2. In a type context, if α is bound to an imported module, then α._id_ is bound to the type bound to _id_ in in the module referred to by α. +3. In a region context, if α is bound to a regime, then α._id_ is bound to the inner regime named _id_ in α. + +### Examples + +``` +# Binds 'foo' in module context, global scope. +module foo { + # Binds 't' in expression context, module scope. + def t: time = 10 s; +} + +module bar { + # Binds 'foo' in type context, module scope. + type foo = length; + + # Binds 'foo' in expression context, module scope. + def foo: foo = 3 m; + + # Refers to 'foo' in module context, from outer global scope. + # Binds 'F' in expression context, module scope. + import foo as F; + + # Binds 'quux' in expression context, module scope. + def quux = + # 'let' rebinds 'F' in the subsequent expression context in + # expression scope. + # + # On the right hand side, 'F' is still bound to the module import, + # and 'u', a record field name, is bound in record context in the + # scope of the record value construct. + # + # 'F.t' is a qualified identifier, that is bound to the constant 't' + # defined in the module 'foo'. + let F = { u = F.t; }; + + # 'F' refers to the record above; 'F.u' is a qualified identifier + # that refers to the value bound to the field 'u' in 'F'. + F.u / 20 s; + + # Error: foo cannot refer to both a value and an imported module in module scope. + import foo; + + # Error: foo cannot refer to both a value and a function in module scope. + def foo = fn () → 4; +} +``` + +## Types and literals + + +Every expression has a type, which is either: + +1. Boolean. +2. A quantity. +3. A record type, comprising an unordered sequence of named fields, with each field being either a quantity or another record type. +4. A function. + +A type expression _type-expr_ identifies a particular type, and is used in type assertions and function argument specifiers. Function types have no corresponding type expression: expressions of a function type may only be bound to an identifier or used in a function application expression. In particular, they may not be used as an argument in a function application. + +A _type-expr_ is either `boolean`, a quantity term, a record type description, or a (qualified) identifier bound to a type expression by a [type alias](#type-aliases). + +> _type-expr_ ::= `boolean` | _quantity-term_ | _record-type-expr_ | _qualified-identifier_ + +An expression of a given type can be constructed from type literals and constructors described below, as well as from operators acting on subexpressions (see the section _Expressions_). + +In definitions of record fields, function arguments, and optionally within expressions a _type-assertion_ declares that the identifier or expression has a given type. + +> _type-assertion_ ::= `:` _type-expr_ + +If the type of an expression bound to an identifier is neither the same as nor a subtype of the type in the assertion, then the binding is ill-formed. Sub- and supertypes constitute a relation between record types, described below. + +Examples of type assertions: + +``` +# Valid: 3 m has type `length`. +def a: length = 3 m; + +# Valid: 3 m has type `length`. +def b = 3 m: length; + +# Valid: the type `small` is a supertype of `big` and the +# function `f` has result of type `length`. +type big = { a: real; b: { x: length; y: length; }; c: mass; }; +type small = { c: mass; b: { x: length; } }; +def f = fn (p: small) → p.b.x + 2 m; +def g = fn (q: big) → f(q) : length; + +# Ill-formed: rhs is not of type `length` +def c: length = 3; +``` + +A quantity type or record has an associated _derivative type_: + +* The derivative type of a quantity type _Q_ is _Q_/ti + +* The derivative type of a record type with fields _fᵢ_ of types _Tᵢ_ is the record type with fields _fᵢ_' and types _Uᵢ_ which are the derivative types of _Tᵢ_. + +### Boolean + + +The boolean type has two possible values, true and false, and expressions of boolean type are constructed from the boolean literals and comparison expressions. + +> _boolean-literal_ ::= `true` | `false` + +The boolean literals are keywords in an expression context, and may not be used as identifiers in this context. + +### Quantities + + +Quantities represent physical quantities, which in turn comprise a magnitude and a physical dimension. The specific unit scale underlying the representation of a physical quantity is implicit. + +A quantity type is defined as a product term of named quantities such as voltage, time, resistance, etc. The set of named quantities is predefined, and cannot be extended within Arblang. + +> _quantity-term_ ::= _quantity-name_ _integer-exponent_? | _quantity-product_ | _quantity-quotient_ +> +> _quantity-product_ ::= _quantity-term_ ( ***whitespace*** | ***multiplication-dot*** ) _quantity-term_ +> +> _quantity-quotient_ ::= _quantity-term_ ***division-slash*** _quantity-term_ +> +> _integer-exponent_ ::= `^` ***minus-sign***? ***numeric-literal*** | ***superscript-literal*** +> +> _quantity-name_ ::= `real` | `length` | `mass` | `time` | `current` | `temperature` | `amount` | +> `frequency` | `area` | `volume` | `velocity` | `acceleration` | `momentum` | `force` | `pressure` | `power` | `energy` | +> `entropy` | `charge` | `voltage` | `capacitance` | `inductance` | `resistance` | `conductance` | `molarity` + +The ***numeric-literal*** in an _integer-exponent_ term must be integral — the token value may not contain a _decimal_separator_ or _exponent_. A non-integral exponent is a syntax error. + +Here, `real` denotes the dimensionless (scalar) quantity. + +The named quantities above are chosen to represent ISQ quantities, but in some cases a single word is used to represent a longer ISQ quantity name to simplify the grammar. The named quantities are listed below with their equivalent ISQ quantity and dimensional expression in terms of the physical dimensions **L** (length), **M** (mass), **T** (time), **I** (electric current), **Θ*** (thermodynamic temperature), and **N** (amount of substance). + +| Arblang name | ISQ name (if different) | ISO document | Dimension | +|----------------|---------------------------|--------------|----------------| +| `real` | quantity of dimension one | 80000-1 | **1** | +| `length` | | 80000-1 | **L** | +| `mass` | | 80000-1 | **M** | +| `time` | | 80000-1 | **T** | +| `current` | electric current | 80000-1 | **I** | +| `temperature` | thermodynamic temperature | 80000-1 | **Θ** | +| `amount` | amount of substance | 80000-1 | **N** | +| `frequency` | | 80000-3 | **T⁻¹** | +| `area` | | 80000-3 | **L²** | +| `volume` | | 80000-3 | **L³** | +| `velocity` | | 80000-3 | **LT⁻¹** | +| `acceleration` | | 80000-3 | **LT⁻²** | +| `momentum` | | 80000-4 | **LMT⁻¹** | +| `force` | | 80000-4 | **LMT⁻²** | +| `pressure` | | 80000-4 | **L⁻¹MT⁻²** | +| `power` | | 80000-4 | **L²MT⁻³** | +| `energy` | kinetic energy | 80000-4 | **L²MT⁻²** | +| | thermodynamic energy | 80000-5 | **L²MT⁻²** | +| `entropy` | entropy | 80000-5 | **L²MT⁻²Θ⁻¹** | +| `charge` | electric charge | 80000-6 | **TI** | +| `voltage` | | 80000-6 | **L²MT⁻³I⁻¹** | +| `capacitance` | | 80000-6 | **L⁻²M⁻¹T⁴I²** | +| `inductance` | | 80000-6 | **L²MT⁻²I⁻²** | +| `resistance` | | 80000-6 | **L²MT⁻³I⁻²** | +| `conductance` | | 80000-6 | **L⁻²M⁻¹T³I²** | +| `molarity` | amount-of-substance concentration | 80000-9 | **L⁻³N** | + +For Arblang, two quantity type expressions are deemed equivalent if they have the same physical dimensionality. Equivalent type expressions describe the same type. + +Quantity literals are composed from a ***numeric-literal*** and an optional _unit-term_ suffix. Units are represented by keywords corresponding to combinations of SI unit prefixes and SI unit abbreviations, and similarly to quantities, are composed via multiplication, division, and integer exponentiation. If no _unit-term_ suffix is present, the quantity is a scalar `real` type (i.e. a quantity of dimension one). + +> _quantity-literal_ ::= ***minus-sign***? ***numeric-literal*** ( ***whitespace*** _unit-term_ )? +> +> _unit-term_ ::= _unit-name_ _integer-exponent_? | _unit-product_ | _unit-quotient_ +> +> _unit-product_ ::= _unit-term_ ( ***whitespace*** | ***multiplication-dot*** ) _unit-term_ +> +> _unit-quotient_ ::= _unit-term_ ***division-slash*** _unit-term_ +> +> _unit-name_ ::= ***symbol*** + +A valid unit name is a ***symbol***, but are _lexically_ described as follows. + +> _unit-name_ ::= _unit-SI-prefix_? _unit-metric_ +> +> _unit-SI-prefix_ ::= `Y` | `Z` | `E` | `P` | `T` | `G` | `M` | `k` | `h` | `da` | `d` | `c` | `m` | `μ` | `u` | `n` | `p` | `f` | `a` | `z` | `y` +> +> _unit-metric_ ::= `m` | `g` | `s` | `A` | `K` | `mol` | `Hz` | `L` | `l` | `N` | `Pa` | `W` | `J` | `C` | `V` | `F` | `H` | `Ω` | `Ohm` | `S` | `M` | `kat` + +Unit prefixes are SI unit prefix symbols, with the addition of `u` for micro-: + +| Unit prefix | SI unit name | Multiple | +|-------------|--------------|----------| +| `Y` | yotta | 10²⁴ | +| `Z` | zetta | 10²¹ | +| `E` | exa | 10¹⁸ | +| `P` | peta | 10¹⁵ | +| `T` | tera | 10¹² | +| `G` | giga | 10⁹ | +| `M` | mega | 10⁶ | +| `k` | kilo | 10³ | +| `h` | hecto | 10² | +| `da` | deca | 10¹ | +| `d` | deci | 10⁻¹ | +| `c` | centi | 10⁻² | +| `m` | milli | 10⁻³ | +| `μ` | micro | 10⁻⁶ | +| `u` | micro | 10⁻⁶ | +| `n` | nano | 10⁻⁹ | +| `p` | pico | 10⁻¹² | +| `f` | femto | 10⁻¹⁵ | +| `a` | atto | 10⁻¹⁸ | +| `z` | zepto | 10⁻²¹ | +| `y` | yocto | 10⁻²⁴ | + +Arblang metric units, and their corresponding Arblang quantities: + +| Unit | Name | Arblang quantity | +|-------|---------|------------------| +| `m` | metre | `length` | +| `g` | gram | `mass` | +| `s` | second | `time` | +| `A` | ampere | `current` | +| `K` | kelvin | `temperature` | +| `mol` | mole | `amount` | +| `Hz` | hertz | `frequency` | +| `L` | litre | `volume` | +| `l` | litre | `volume` | +| `N` | newton | `force` | +| `Pa` | pascal | `pressure` | +| `W` | watt | `power` | +| `J` | joule | `energy` | +| `C` | coulomb | `charge` | +| `V` | volt | `voltage` | +| `F` | farad | `capacitance` | +| `H` | henry | `inductance` | +| `Ω` | ohm | `resistance` | +| `Ohm` | ohm | `resistance` | +| `S` | siemens | `conductance` | +| `M` | molar | `molarity` | +| `kat` | katal | `amount/time` | + +Note that the non-SI unit 'molar' is equal to 1 mol/L. + +As a possible extension, Arblang might support non-zero based units such as degrees Celsius °C. Doing so, however, complicates the algebra; refer to the [appendix](#extension-offset-values-and-affine-spaces). + +#### Magnitudes + +The magnitude of a quantity is a member of an extended real number set _R_, where _R_ = ℝ ∪ {-∞, +∞} ∪ {⊥}. Positive and negative infinity describe the extrema in the order completion of the reals, while ⊥ represents the 'not a number' value. Any partial function _f_: ℝ → ℝ can be extended to a total function _f⁺_: _R_ → _R_ by: + +1. _f⁺_(_x_) = _f_(_x_) for all _x_ in the domain of _f_. +2. _f⁺_(⊥) = ⊥ +3. For _a_ equal to ∞, -∞, or in the complement of the domain of _f_, if lim *x*→*a* *f*(*x*) = _L_ for _L_ in ℝ or where _L_ is ∞ or -∞, then _f⁺_(_a_) = _L_ in _R_. Otherwise, _f⁺_(_a_) = ⊥. + +Functions of more than one variable are extended similarly. Arithmetic operations are extended as usual to ℝ ∪ {-∞, ∞}, with the value of indeterminite forms taking the value ⊥. The value of any expression involving ⊥ is ⊥. + +When interpreted or compiled into an Arbor mechanism, _R_ and operations upon it will necessarily be approximated in some manner; IEEE 754 semantics are a reasonable expectation, with NaN representing ⊥, but the interpreter or transpiler is permitted to perform algebraic simplifications including: + +1. Reordering of associative operations. +2. Constant folding. +3. Algebraic elimination of terms (which may change the value of some expressions from ⊥ to a value in ℝ ∪ {-∞, ∞}, or from an infinite value to a finite value). + + +### Records + + +A record is a labelled unordered tuple of values which are either quantities or records themselves. A record may not have two fields of the same name. A record type specification has the syntax: + +> _record-type-expr_ ::= `{` _field-spec_* `}` +> +> _field-spac_ ::= ***symbol*** _type-assertion_ `;` +> +> _type-assertion_ ::= `:` _type-expr_ + +A record type _R_ with fields _fᵢ_ of type _Tᵢ_ is a supertype of a record type _S_ with fields _gⱼ_ of type _Uⱼ_ if for every _i_ there exists a _j_ such that _fᵢ_ and _gⱼ_ have the same identifier and _Tᵢ_ is the same type as or a supertype of _Uⱼ_. If _R_ is a supertype of _S_ and _S_ is a supertype of _R_, then _R_ and _S_ are the same type. Note that the order of fields in a _record-type_ is arbitrary. + +Correspondingly, record literals have the syntax: + +> _record-literal_ ::= `{` _field-defn_* `}` +> +> _field-defn_ ::= ***symbol*** _type-assertion_? `=` _expression_ `;` | _reaction_ `;` + +For field definitions, if there is no type assertion given, the type of the field is deduced from the expression on the right hand side. + +The field names constituting the left hand side of the field definitions have the _record scope_ of the record value. The defining expressions on the right hand side remain in an expression context, so that identifiers with the same symbol as a record field will _not_ refer to that record. For example, in the expression + +``` +let a = 3 m; +let r = { a = 4; b = a; }; +r.b +``` + +`r` has type `{ a: real; b: length; }` and is bound to the value `{ a = 4; b = 3 m; }`, because the `a` in the right hand side of `b = a` is in expression context, and so is bound to to the value 3 m as given in the outer `let`. + +Field values in a record are accessed via a qualified identifier (see [Qualified identifiers](#qualified-identifiers) above), or by immediate field access (see [Record expressions](#record-expressions) below), or brought into scope via a `with` binding (see [Value bindings](#value-bindings), below). + +``` +let r = { a = 4; }; r.a # qualified identifier evaluates to value 4 +let x = { a = 4; }.a; x # immediate field access evaluates to value 4 +with { a = 4; }; a # a is locally bound to the value 4 +``` + +#### Chemical equation syntax + +> _reaction_ ::= _right-reaction_ | _left-reaction_ | _right-left-reaction_ +> +> _right-reaction_ ::= _complex_ ***right-arrow*** _complex_ `(` _expression_ `)` +> +> _left-reaction_ ::= _complex_ ***left-arrow*** _complex_ `(` _expression_ `)` +> +> _right-left-reaction_ ::= _complex_ ***right-left-arrow*** _complex_ `(` _expression_ `,` _expression_ `)` +> +> _complex_ ::= ***empty-set*** | ***numeric-literal***? ***symbol*** ( `+` ***numeric-literal***? ***symbol*** )* + +A _reaction_ clause describes a chemical reaction equation between multisets (complexes) of species. In the context of a record literal, _reaction_ clauses are translated into field definitions through a process described below. For ease of algebraic manipulation in the determination of ODE solutions and steady states, it can be useful to retain a representation of the untranslated reactions themselves together with the internal record representation. + +A _complex_ is zero (represented by ***empty-set***) or more species names each represented by a ***symbol***, possibly prefixed by a positive integer coefficient, and separated by ***plus-sign***. A ***numeric-literal*** in a _complex_ term that is not a positive integer is a syntax error. The corresponding multiset comprises these species, with the coefficient determining the multiplicity. + +A reaction may be a _right-reaction_, a _left-reaction_, or a _right-left-reaction_. For a _right-reaction_ or _left-reaction_, the _expression_ in parentheses is the reaction rate coefficient. A _left-reaction_ of the form `complex₁ ← complex₂ (expr)` is exactly equivalent to a _right-reaction_ of the form `complex₂ → complex₁ (expr)`. For a _right-left-reaction_, the first _expression_ in the parenthesis is the forward reaction coefficient and the second is the reverse reaction coefficient. A _right-left-reaction_ of the form `complex₁ ⇄ complex₂ (expr₁, expr₂)` is exactly equivalent to a _right-reaction_ `complex₁ → complex₂ (expr₁)` and a _left-reaction_ `complex₁ ← compex₂ (expr₂)`. + +#### Converting reaction clauses to field definitions + +In a record literal, each species _α_ present in any reaction clause complex will generate a field definition for the field named _α'_. The identifier _α_ will represent a species concentration, and _α'_ its rate of change. + +Consider the normalized representation of the set of reaction clauses, where each is represented by one or two right reactions of the form _Lᵢ → Rᵢ (κᵢ)_, where are _Lᵢ_ and _Rᵢ_ are complexes. Let Π*C* denote the product with multiplicity of the species terms in a complex *C*, and *μ*(*α*; *C*) the multiplicity of a species _α_ in _C_. + +The expression assigned to _α'_ in its field definition is the sum of terms _κᵢ_·Π*Lᵢ*·(*μ*(*α*; *Rᵢ*) - *μ*(*α*; *Lᵢ*)) for each reaction _i_. + +Example: consider the reaction system below involving three species _a_, _b_ and _c_, represented by their concentrations, coupled via a reaction rate to a quantity _x_ that is governed also by a simple ODE. + +``` +{ + x' = 1.23 M⁻³s⁻²; + 2a + b + c → 2b (x); + ∅ → c (3.4 M/s); +} +``` + +The record literal is then algebraically equivalent to the following. + +``` +{ + x' = 1.23 M⁻³s⁻²; + a' = -2·x·a²·b·c; + b' = x·a²·b·c; + c' = -x·a²·b·c + 3.4 M/s; +} +``` + +### Functions + + +A function literal gives a value of a function type. Function types have no representation in the Arblang source language, and so cannot be used in type assertions, or in function arguments. Function literals may only appear in _function-application_ expressions or as the bound value in a _let-binding_ or module _function-defn_. + +> _function-literal_ ::= `fn` `(` ( _function-arg_ ( `,` _function-arg_ )* )? `)` ***right-arrow*** _expression_ | `(` _function-literal_ `)` +> +> _function-arg_ ::= ***symbol*** _type-assertion_ + +The identifiers introduced by _function-arg_ clauses have function scope which comprises the final defining expression. These are bound to parameter values in a function call expression (see _Expressions_ below). The final expression may be of any non-function type, but may involve identifiers bound only to: other functions, _parameter-constant_ expressions, or the function arguments. In particular, the expression may not contain identifiers bound to an external _bindable_ in an interface. + + +## Expressions + + +The expression syntax below is ambiguous in that, for example, a function application or qualified identifier may be parsed as a _boolean-expr_, _algebraic-expr_, or _record-expr_. Each possible parse should be semantically equivalent. + +> _expression_ ::= ( _value-binding_ | _conditional-expr_ | _boolean-expr_ | _algebraic-expr_ | _record-expr_ ) _type-assertion_? | `(` _expression_ `)` + +An expression with type assertion of the form `expr: T` is valid if the type of `expr` is `T` or a supertype of `T`, and ill-formed otherwise. The type of `expr: T`, if well-formed, is always the type `T`. + +Each identifier or qualified identifier in an expression must be bound (in the context determined by its occurrence). In expression context, the identifier or qualified identifier may be bound to a function argument, to another expression via a value binding in an outer expression, to a record field, to a module constant or function definition, to a module parameter, or to an external quantity via an interface binding. + +An expression is a _constant_ expression if every identifier in the expression is bound to a module constant or another constant expression, and if every function application subexpression has a value that is a constant expression. Similarly, an expression is _parameter-constant_ if every identifier is bound to a module constant or parameter, or another parameter-constant expression, and if every function application has a value that is parameter-constant. + +### Value bindings + + +> _value-binding_ ::= _let-binding_ | _with-binding_ +> +> _let-binding_ ::= `let` ***symbol*** ( _type-assertion_? `=` _expression_ | `=` _function-literal_ ) `;` _expression_ +> +> _with-binding_ ::= `with` _expression_ `;` _expression_ + +Both `let` and `with` introduce new identifiers in expression context that can mask bindings from outer scopes. + +The value of the let expression `let id = expr₁; expr₂` is `expr₂` with `id` bound to `expr₁`. + +The value of the where expression `where expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. + +Example: + +``` +let a = { scale = 3.2; pos = { x = 3 m ; y = 4 m; }; }; # binds `a` below. +with a.pos; # binds `x` to 3 m and `y` to 4 m below. +a.scale*(x+y); +``` + +As the type of a value binding is the type of its final expression, syntactic ambiguity in type assertion parsing has no semantic consequence: `let id = expr₁; expr₂: T` has the type of `expr₂: T`, which is `T` iff the type of `expr₂` is `T` or a supertype of `T` ; similarly, `(let id = expr₁; expr₂): T` has type `T` iff the type of `let id = expr₁; expr₂`, which is the type of `expr₂` is `T` or a supertype of `T`. + + +### Conditional expressions + + +> _conditional-expr_ ::= _if-expr_ | _case-expr_ +> +> _if-expr_ ::= `if` _boolean-expr_ `then` _expression_ `else` _expression_ +> +> _case-expr_ ::= `|` _boolean-expr_ ***right-arrow*** _expression_ )? _case-expr_ | `|` ( `otherwise` | `true` ) ***right-arrow*** _expression_ + +Alternatives based on one or more conditions can be expressed with if/then/else clauses or case expressions introduced with the bar symbol. In either, the conditional expression is ill-formed if any of the _boolean-expr_ have type which is not boolean. + +The value of `if condition then expr₁ else expr₂` is the value of `expr₁` in the case where `condition` is true, and `expr₂` otherwise. The type of the _if-expr_ is the type of `expr₁` and `expr₂`; the expression is ill-formed if the types of `expr₁` and `expr₂` differ. + +The value of `| otherwise → expr` is just the value of `expr`. `true` can be used in place of `otherwise` equivalently. For a compound _case-expr_ of the form `| condition → expr₁ case₂`, the value is `expr₁` in the case where `condition` is true, and the value of `case₂` otherwise; the expression is ill-formed if the types of `expr₁` and `case₂` differ. + +Example: + +``` +# Equivalent to 10 km: +let a = if 3>2 then 10 m else 2 m; a*1000 + +# Piece-wise constant reaction rate function. +def rate = fn (T: temperature) → + | T < 0 °C → 10 mM/s + | T < 10 °C → 20 mM/s + | otherwise → 30 mM/s; + +``` + +As with value bindings, there is no semantic ambiguity arising from an ambiguous parse from a trailing type assertion. + + +### Boolean expressions + + +> _boolean-expr_ ::= _boolean-term_ ( `or` _boolean-term_ )* +> +> _boolean-term_ ::= _boolean-factor_ ( `and` _boolean-factor_ )* +> +> _boolean-factor_ ::= `not`? ( _comparison-expr_ | _function-application_ | _qualified-identifier_ | _boolean-literal_ | `(` _boolean-expr_ `)` ) +> +> _comparison-expr_ ::= _comparison-base_ _comparison-op_ _comparison-base_ +> +> _comparison-op_ ::= ***compare-equal*** | ***compare-not-equal*** | ***compare-less*** | ***compare-less-equal*** | ***compare-greater*** | ***compare-greater-equal*** +> +> _comparison-base_ ::= _algebraic-expr_ | `(` _expression_ `)` + +A compound boolean expression of the form `expr₁ or expr₂` is well defined only if the types of `expr₁` and `expr₂` are both boolean. The value is false if both `expr₁` and `expr₂` have value false, and true otherwise. The `or` operation can be considered to be left associative, but the `or` operation is both commutative and associative. + +The boolean operator `and` has higher precedence than that of `or`, and `expr₁ and expr₂` has value true iff `expr₁` has value true and `expr₂` has value true. The expression is ill-formed if `expr₁` or `expr₂` do not have type boolean. Similarly to `or`, the operator can be considered to be left-associative, but there is no ambiguity regardless. + +`not` has the highest precedence of the boolean operators, and `not expr` has value true iff `expr` has value false. The expression is ill-formed if `expr` does not have type boolean. + +A _comparison-expr_ of the form `expr₁ == expr₂` or `expr₁ ≠ expr₂` is well-defined iff `expr₁` and `expr₂` have the same type, with that type being a quantity type, a record type, or boolean. Its value is true if the two expressions have the same boolean or quantity values or if the expressions are of the same record type and `(expr₁).f == (expr₂).f` for each field `f` in this record type, and is otherwise false. `expr₁ ≠ expr₂`, if well-defined, is true iff `expr₁ == expr₂` is false. + +A _comparison-expr_ of the form `expr₁ op expr₂` where `op` is not `==` nor `≠` is well-defined iff `expr₁` and `expr₂` have the same quantity type. The comparison operators `≥`, `>`, `≤`, `<` respect the usual ordering on real numbers, after applying any requisite scaling to equate units. + +When a _comparison-expr_ `expr₁ op expr₂` compares two terms of the same quantity type which may carry an offset value from a non-zero based unit, the value is equivalent to `expr₁ - expr₂ op zero` where `zero` is a zero-valued quantity of the same type as `expr₁`. See [Offset units](#offset-units) below. + +A _boolean-expr_ may not involve any boolean or comparison operations, and be equivalently parsed as an algebraic expression. In this instance, its type and value is the same as if it were parsed directly as an algebraic expression. + + +### Algebraic expressions + + +> _algebraic-expr_ ::= _algebraic-term_ ( ( ***plus-sign*** | ***minus-sign*** ) _algebraic-term_ )* +> +> _algebraic-term_ ::= _algebraic-factor_ ( ( ***multiplication-dot*** | ***asterisk*** | ***division-slash*** ) _algebraic-factor_ )* +> +> _algebraic-factor_ ::= _quantity-literal_ | ( ***minus-sign*** | ***square-root*** )* _algebraic-base_ _algebraic-exponent_? ) +> +> _algebraic-base_ ::= _function-application_ | _qualified-identifier_ | _record-field-expr_ | ***numeric-literal*** | `(` _expression_ `)` +> +> _algebraic-exponent_ ::= ***superscript-literal*** | ( `^` _algebraic-factor_ )+ + +Additive operators `+` and `-` and multiplicative operators `*` (or `·`) and `/` are all left associative. Multiplicative operators have higher precedence than additive operators. + +An additive expression of the form `expr₁ + expr₂` or `expr₁ - expr₂` is well formed iff `expr₁` and `expr₂` have the same quantity type. The expression has the same quantity type, with the value corresponding to the regular arithmetic operation after any requisite scaling to equalize units. For values that may carry an offset from a non-zero based unit, refer to [Offset units](#offset-units) below. + +A multiplicative expression of the form `expr₁·expr₂` or `expr₁/expr₂` is well defined if `expr₁` and `expr₂` have types _T₁_ and _T₂_ respectively, both of which are quantity types. The resultant type is the quantity-type _T₁·T₂_ or _T₁/T₂_ accordingly. + +A power expression of the form `expr₁^expr₂` is well formed iff `expr₁` and `expr₂` are both of type real or `expr₁` has a quantity type and `expr₂` is an integer valued constant expression (but see [Fractional powers for quantities and units](#fractional-powers-for-quantities-and-units)). A power expression with a superscript exponent is defined similarly. + +Unary minus is arithmetically equivalent to multiplication by minus one; in particular, if _x_ in the expression `-x` is a value with offset type, it is interpreted as a difference quantity, not an absolute quantity, and any offset is ignored. + +The square root is introduced by ***square-root*** , and an expression `√x` is arithmetically equivalent to `x^(1/2)`. + +The value of an additive, multiplicative or power expression follows the usual calculi of physical quantities (for one of a number of formal treatmes, see for example, P Szekeres, _The mathematical foundations of dimensional analysis and the question of fundamental units_, International Journal of Theoretical Physics 17 no. 12 (1978), doi:10.1007/BF00678423, pp. 957–974). + +> _function-application_ ::= ( _qualified-identifier_ | `(` _function-literal_ `)` ) `(` ( _expression_ ( `,` _expression_ )* )? `)` + +A _function-application_ expression is well-formed iff the function type of the _function-literal_ or the function value bound to _qualified-identifier_ is compatible with the number and types of the _expression_ clauses constituting the arguments. If the function value corresponds to the form `fn (a₁: T₁, …) → result`, then the value of the function application expression with arguments `expr₁`, … is the value of the expression `let a₁: T₁ = expr₁; … result`. + + +### Record expressions + + +> _record-expr_ ::= _record-term_ ( ***preferential-union*** _record-term_ )* +> +> _record-term_ ::= _record-literal_ | _function-application_ | _qualified_identifier_ | _record-literal_ | `(` _record-expr_ `)` +> +> _record-field-expr_ ::= ( _record-literal_ | _function-application_ | `(` _record-expr_ `)` ) `.` _qualified-identifier_ + +Access to a field in a record that is bound to an identifier can be made via the corresponding qualified identifier (see section _Qualified Identifiers_); for records that are not bound to an identifier, the _record-field-expr_ provides the same function, also using the period as an field access operator. + +Records of different types can be combined with the ***preferential-union*** operator: given a record _r_ with fields _fᵢ_ and values _vᵢ_ for _i_∈_I_, and another record _s_ with fields _gⱼ_ and values _wⱼ_ for _j_∈_J_, the expression _r_ ⊔ _s_ is a record with a set of fields {_fᵢ_}∪{_gⱼ_}, and the value of a field _h_ in this record is _vᵢ_ if there exists a field _fᵢ_=_h_, else _wⱼ_ for the field _wⱼ_=_h_. Essentially, the record comprises all the fields of the left hand side, together with any fields from the record on the right hand side which don't have the same name as a field in the first record. + + +### Precedence + + +Where this is ambiguity in expression parsing, operators should be considered in the following order of decreasing precedence. In the table, _f_, _j_, _x_ and _y_ stand for expressions of the appropriate type. + +| Operator | Description | Associativity | Notes | +|----------------------------|--------------------------|---------------|-| +| _x_`.`_y_ | Record field | left | | +| _f_`(`…`)` | Function application | left | [1](#precedence-note-1) | +| _x_`^`_y_, _xʲ_ | Exponentiation | right | [2](#precedence-note-2) | +| `-` | Unary minus | right | [3](#precedence-note-3) | +| `√` | Square root | right | [3](#precedence-note-3) | +| _x_`·`_y_, _x_`/`_y_ | Product, quotient | left | | +| _x_`+`_y_, _x_`-`_y_ | Sum, difference | left | | +| `⊔` | Preferential union | left | | +| `<`, `≤`, `>`, `≥` | Order comparitsons | left | | +| `==`, `≠` | Compare equal, not equal | left | | +| `not` | Logical not | right | | +| `and` | Logical and | left | | +| `or` | Logical or | left | | +| `:` _type-expr_ | Type assertion | left | | +| `if` _x_ `then` y `else` z | Ternary conditional | right | | +| `\|` _x_ → _y_ | Case expression | right | | +| `let`, `with` | Value bindings | right | | + +Notes: + +1. Function application can be considered left associative in accordance with mathematical convention, but it cannot arise while function values are unable to be returned from an Arblang function. + +2. Multiple exponentiation by superscript literal should be prohibited by the _alegebraic-exponent_ syntax rule. + +3. Multiple adjacent unary minus operators should be prohibited by the _algebraic-factor_ syntax rule. + + +### Built-in functions + +Arblang includse some predefined real functions, already bound in each module scope: + +| Function | Operation | +|--------------------|---------------------------------------------------------| +| `abs(x: real)` | Absolute value \|*x*\| | +| `sin(x: real)` | Sine of _x_ in radians | +| `cos(x: real)` | Cosine of _x_ in radians | +| `tan(x: real)` | Tangent of _x_ in radians | +| `asin(x: real)` | Inverse sine in range [-π/2, π/2] | +| `acos(x: real)` | Inverse cosine in range [0, π] | +| `atan(x: real)` | Inverse tangent in range (-π/2, π/2) | +| `exp(x: real)` | Natural exponential e^x of _x_ | +| `expm1(x: real)` | *e*^*x* - 1 (for small *x*) | +| `exprel(x: real)` | Relative exponential ₁F₁(1; 2; *x*) = (*e*^*x* - 1)/*x* | +| `exprelr(x: real)` | Reciprocal relative exponential 1/₁F₁(1; 2; *x*) | +| `log(x: real)` | Natural logarithm of _x_ | +| `logp1(x: real)` | log(*x* + 1) (for small *x*) | +| `sinh(x: real)` | Hyperbolic sine of _x_ | +| `cosh(x: real)` | Hyperbolic cosine of _x_ | +| `tanh(x: real)` | Hyperbolic tangent of _x_ | +| `asinh(x: real)` | Inverse hyperbolic sine of _x_ | +| `acosh(x: real)` | Inverse hyperbolic cosine of _x_ | +| `atanh(x: real)` | Inverse hyperbolic tangent of _x_ | + +In addition, it provides the function `nernst(z: real, T: temperature, Cinner: concentration, Couter: concentration)` defined as _R_·_T_/_z_·(log _Cinner_ - log _Couter_), where _R_ is the molar gas constant as defined in the 2019 SI units as exactly 8.314'462'618'153'24 J/K/mol. + +## Modules and interfaces + + +Modules are used to collect parameters, constants, and function definitions; interfaces are used to define a particular sort of Arbor functionality, such as ion channel or gap junction dynamics. Module and interface definitions can only be provided at top level. + + +### Module definition + + +> _module-defn_ ::= `module` ***symbol*** `{` _module-decl_* `}` +> +> _module-decl_ ::= _type-alias_ | _parameter-defn_ | _constant-defn_ | _function-defn_ | _module-import_ +> +> _module-import_ ::= `import` ***symbol*** ( `as` ***symbol*** ) +> +> _type-alias_ ::= `type` ***symbol*** `=` _type-expr_ `;` +> +> _parameter-defn_ ::= `parameter` ***symbol*** _type-assertion_? `=` _expression_ `;` +> +> _constant-defn_ ::= `def` ***symbol*** _type-assertion_? `=` _expression_ `;` +> +> _function-defn_ ::= `def` ***symbol*** `=` _function-literal_ `;` + +#### Module import + + +Identifiers bound in module scope in one module can be used in another module or interface, if the module is imported. If a module `A` is imported as `B`, a type, parameter, constant, or function _x_ defined in `A` can be referenced with the qualified identifier `B`._x_. + +Examples: +``` +module A { + constant real pi = 3; +} + +module X { + import module A; + constant real pi = A.pi; # Also 3. +} + +module Y { + import module A as B; + constant real pi = B.pi; # Also 3. +} +``` + +Note that in a module import `import module A as B`, `A` is interpreted in module context, while `B` is interpreted in expression context. So the following is well-formed, +``` +module A { } +module B { + def A = 3; + import A as M; +} +``` +but +``` +module A { } +module B { + def M = 3; + import A as M; +} +``` +is not, as `M` is being rebound in module scope in an expression context. + + +#### Type aliases + + +A type alias binds a non-function type to an identifier in module scope, in type contexts. In addition, if the bound type is a record or quantity type, the derivative type of the bound type is bound to the identifier suffixed with an apostrophe `'` (or equivalently, any of the accepted prime marks). + +Example: +``` +type foo = metre; +type bar = { a: time; b: foo }; + +# type aliases used to assert type in constant definitions: +def r: foo = 10 m; +def s: bar = { a = 3 s; b = 20 m; }; + +# derivative type aliases are bound implicitly: +def r': foo' = 1 m/s; +def s': bar' = { a' = 1.2; b' = 3.4 m/s; }; + +``` + +#### Parameters + +A parameter definition introduces a new identifier in module scope, in expression contexts, together with a default value given by a _paramater-constant_ expression — that is, the expression can depend only upon constants and other parameters (see [Expressions](#expressions)). + +Parameters that are exported in an interface can be bound to a user supplied value externally; they are otherwise constant. In any expression in the same module scope that uses that parameter, the value of the parameter will be the user supplied value. This applies to expressions that are bound to other parameters — for example, consider the following module and interface definition. + +``` +module impl { + parameter a: voltage = 3 mV; + parameter I: current = (13 mV - a) / 20 kΩ; +} + +interface point "foo" { + import impl; + export parameter impl.a as a; + + effect current = impl.I; +} +``` + +Models using the "foo" mechanism can set the parameter `a` to some voltage. If it remains unset, the mechanism supplies a non-specific current of 0.5 μA; if the model sets the parameter `a` to -7 mV, the parameter `I` in the `impl` module will have the value 1.0 µA, which will in turn be the supplied non-specific current. + +#### Constant and function definitions + + +The `def` keyword introduces new bound identifiers in module scope, in expression contexts. + +Function definitions may not take a type assertion, but constant definitions may. For constant definitions, the bound value must be a _constant-expression_ (see [Expressions](#expressions)). + +``` +def a: length = 10 m; # Constant definition. +def sq = fn (x: real) → x² # Function definition. + +parameter P = 1.23; + +# The following definition is ill-formed, as the bound expression depends upon a parameter, and so is not a constant expression. +def b: real = 2*sq(P); +``` + +### Interface definition + + +> _interface-defn_ ::= `interface` _interface-class_ _string-literal_ `{` _interface-decl_* `}` +> +> _interface-class_ ::= `density` | `discrete` | `concentration` +> +> _interface-decl_ ::= _module-decl_ | _export_ | _export-parameter-defn_ | _external-binding_ | _effect-defn_ | _initial-defn_ | _regime-defn_ | _regime-decl_ +> +> _export_ ::= `export` _export-qualifier_* `parameter` _qualified-identifier_ _type-assertion_? ( `as` ***symbol*** )? +> +> _export-parameter-defn_ ::= `export` _export-qualifier_* _parameter-defn_ +> +> _export-qualifier_ ::= `density` +> +> _external-binding_ ::= `bind` _identifier_ _type-assertion_? = _bindable_ `;` +> +> _bindable_ ::= `state` | `membrane` `potential` | `temperature` | (`current` `density` | `molar` `flux`) _species-name_ | (`internal` | `external`) `concentration` _species-name_ | `charge` _species-name_ +> +> _initial-defn_ ::= `initial` ( `regime` `=` _qualified-identifier_ `;` )? ( _initial-post-expr_ `from` )? `state` _type-assertion_? `=` _expression_ `;` +> +> _initial-post-expr_ ::= `steady` | `evolve` `for` _expression_ +> +> _regime-defn_ ::= `regime` _identifier_ `{` ( _regime-decl_ | _regime-defn_ )* `}` +> +> _regime-decl_ ::= _evolve-defn_ | _when-defn_ | _effect-defn_ +> +> _evolve-defn_ ::= `evolve` `explicit`? `state'` _type-assertion_? `=` _expression_ `;` +> +> _when-defn_ ::= `when` _when-condition_ ( `regime` = _qualified-identifier_ `;` )? `state` `=` _expression_ `;` +> +> _when-condition_ ::= _boolean-expr_ | _identifier_ _type-assertion_ = _external-event_ `;` +> +> _external-event_ ::= `event` | `post` +> +> _effect-defn_ ::= `effect` _effect_ = _expression_ `;` +> +> _effect_ ::= `current` `density` _species-name_? | `molar` `flux`_species-name_ | `current` _species-name_? | `molar` `flow` `rate` _species-name_ | (`internal` | `external`) `concentration` `rate` _species-name_ +> +> _species-name_ ::= ***string-literal*** + +Definitions and bindings in interface definitions, much like in modules, have module scope. In addition to the restriction on rebinding identifiers in module scope, interface declarations have the following restrictions: + +* The same identifier cannot be bound with `bind` more than once. + +* The same _effect_ can not be defined more than once. + +In the module context of an interface, the identifier `state` is already bound in an expression context to the _bindable_ `state`, and is bound to the type of the _bindable_ `state` in a type context. `state'` is the implicitly defined type alias for the derivative type of `state`. This does not preclude other bindings to the _bindable_ `state`. + +#### Initial definition + +The value bound to `state` in an _initial-defn_ must be of a record or quantity type. This value defines or is used to compute the initial value of the initial value problem defined by interface `evolve` and `when` definitions. The type of this value determines the type of the bindable state and the state derivative expression used in an _evolve-defn_. + +The initial regime is determined by the _regime_ clause; if none is given, the initial regime is the unnamed top-level regime. + +If there is an _initial-post-expr_ `steady`, the initial state value is derived from the provided state value _s_ as a steady-state solution to the initial value problem with value _s_ at time zero and any bound interface values held constant. + +If there is an _initial-post-expr_ `evolve for t` for some expression _t_, the initial state value is derived from the provided state value _s_ as the solution at time _t_ of the initial value problem with value _s_ at time zero and any bound interface values held constant. The expression _t_ must be parameter-constant. + +If the interface has no _initial-defn_ at all, the initial state is defined to be the empty record `{}`. + +#### Regime definitions + +A regime defines the dynamical evolution of the mechanism state, and the effects of the mechanism state on the cellular state. There is always a top-level, unnamed regime, but more regimes can be introduced with a _regime-defn_. Associated with each regime is an evolution definition and a set of conditions that determine behaviour upon an external event or the satisfaction of some predicate. + +A regime definition introduces a new regime scope: inner regimes may be given names that mask outer regime names, and regime transitions in `when` clauses can refer to regimes defined in outer scopes without further qualification. A transition can also refer to a regime in the interface by using a qualified identifier: + +``` +regime A { + regime B { + regime C { + } + } + + regime D { + # regime B is defined in outer scope. + when p(state) regime = B.C; state = f(state); + } +} + +regime E { + # regime A is defined in outer scope. + when q(state) regime = A.D; state = g(state); +} +``` + +If an evolution is not specified in a regime, the evolution will be that of the outer regime. Similarly, any effects defined in an outer regime will apply, if the same effect is not defined within the inner regime. The topmost unnamed regime will implicitly define an evolution if none is provided: this implicit evolution will hold the state constant over time. + +Any `when` conditions defined in an outer regime, including the topmost unnamed regime, still apply in inner regimes. + +#### When semantics + +When clauses are triggered when the mechanism state satisfies the corresponding predicate, or when an event of the appropriate type is delivered to the mechanism. The state is updated according to the `state = ` clause, and if a `regime` clause is present, the dynamics are shifted to the given regime. + +A given when clause associated with a regime _R_, with predicate _p_ applies at the point in time _t₁_ if the dynamics are in regime _R_ at _t₁_, _p_(_t₁_) is true and either _p_(_t_) is false or dynamics were in a regime _R'_ without this when clause for _t_ ∈ (_t₁_-δ, _t₁_) for some δ>0. All predicates are considered false for _t_ < 0. + +If more than one when clause applies, they are applied in order of definition. Note that the effect of a when clause may cause a transition to a regime where the set of applicable when-clauses differs, whence the new set is considered in its stead. In any instance, no single when clause may be triggered more than once by the same event or, for predicate-based when clauses, at the same time. + +Consider the following situation: +``` +initial regime X state = 0; + +regime X { + when ev = event; state = 1; # (A) + when ev = event; regime = Y; state = 2; # (B) + when ev = event; state = 3; # (C) + when state == 4 regime = Y; state = 5; # (D) +} + +regime Y { + when true regime = X; state = 4; # (E) +} +``` + +On the first event, when clauses (A) and (B) will be triggered, transitioning to regime Y with state equal to 2. At this point, the event has been handled. However the clause (E) becomes applicable as soon as the evolution is considered, and state is set to 4, and regime transitions back to X. Clause (D) now applies, setting state to 5, and transitioning back to regime Y. However clause (E) has already been triggered at this time, and so cannot be applied again. + +#### Evolution + +An evolution definition determines how the mechanism state changes in time (up until any event or predicate triggers a when clause). In the initial version of Arblang, the only supported description of these dynamics is via an explicit ODE system of the form d*s*/d*t* = _f_(_s_; _p₁_, _p₂_, ...) where _s_ represent the state value and _p₁_, … are values associated with the cellular state and made available via a `bind` clause. + +In a definition `evolve state' = expr;`, the right hand side `expr` must have the derivate type of the type of the mechanism state. It may depend upon any parameter, constant or bound identifier including the bound by default identifier `state`. + +As an example, this adaption of an Allen Institute Kv3 channel model has state of type `{ m: real }`, and so the expression in the `evolve` definition must be of the derivative type `{ m': real/time }`. + +``` +interface density "Kv3" { + bind v = membrane potential; + + def minf = fn (v: voltage) → 1/(1 + exp(-(v - 18.7 mV)/9.7 mV); + def mrate = fn (v: voltage) → 0.25 ms⁻¹ * (1+ exp(-(v + 46.56 mV)/44.14 mV)); + + export density parameter gbar = 10⁻⁵ S/cm²; + export parameter ek = -88 mV; + + initial state = { m = minf(v); }; + evolve state' = with state; { m' = (minf(v) - m)·mrate(v); }; + + effect current density "k" = gbar*state.m*(v-ek); +} +``` + +As the state comprises only a single field, an alternative presentation uses just a real value for state: +``` +interface density "Kv3" { + bind v = membrane potential; + + def minf = fn (v: voltage) → 1/(1 + exp(-(v - 18.7 mV)/9.7 mV); + def mrate = fn (v: voltage) → 0.25 ms⁻¹ * (1+ exp(-(v + 46.56 mV)/44.14 mV)); + + export density parameter gbar = 10⁻⁵ S/cm²; + export parameter ek = -88 mV; + + initial state: real = minf(v); + + bind m = state; + evolve state' = (minf(v) - m)·mrate(v); + + effect current density "k" = gbar*m*(v-ek); +} +``` + + + +#### Effects and external bindings + +Effects describe the effect of a mechanism's state on dynamics of the cell on which it acts. Some effects relate to a particular ion (or more generally, chemical species). Species names are described by string literals, and an effect depending upon a species will include that literal as the last part of the _effect_ clause within the definition. + +Possible [external bindings](#external-bindings) are aspects of the cellular state that can influence the cell evolution and the mechanism effects. Most may vary over time, though species charge in particular is guaranteed to be constant over the evolution of mechanism state. + +As noted in [Mechanisms](#mechanisms), not all effects and bindings are available to all interface classes. Permissible external bindings and effects and their quantity types are listed below, where _species_ is a placeholder for a string literal denoting a particular species. + +| External binding | Type | Density? | Discrete? | Concentration? | +|--------------------------------------|--------------------|----------|-----------|----------------| +| `state` | | ✓ | ✓ | ✓ | +| `membrane` `potential` | `voltage` | ✓ | ✓ | ✓ | +| `temperature` | `temperature` | ✓ | ✓ | ✓ | +| `current` `density` _species_ | `current/area` | | | ✓ | +| `molar` `flux` _species_ | `amount/area/time` | | | ✓ | +| `internal` `concentration` _species_ | `molarity` | ✓ | ✓ | ✓ | +| `external` `concentration` _species_ | `molarity` | ✓ | ✓ | ✓ | +| `charge` _species_ | `real` | ✓ | ✓ | ✓ | + + +| Effect | Type | Density? | Discrete? | Concentration? | +|---------------------------------------------|--------------------|----------|-----------|----------------| +| `current` `density` | `current/area` | ✓ | | | +| `current` `density` _species_ | `current/area` | ✓ | | | +| `molar` `flux` _species_ | `amount/area/time` | ✓ | | | +| `current` | `current` | | ✓ | | +| `current` _species_ | `current` | | ✓ | | +| `molar` `flow` `rate` _species_ | `amount/time` | | ✓ | | +| `internal` `concentration` `rate` _species_ | `molarity/time` | | | ✓ | +| `external` `concentration` `rate` _species_ | `molarity/time` | | | ✓ | + + +# Extensions and alternatives + +## Magic keywords and interface extension points + +Within an interface block, there are specific points within the permitted syntax where keywords are used to refer to interface-specific values or concepts, and which constitute natural places for future extensions of the interface block to support new functionality: + +1. Right hand side of `bind`, corresponding to interface-specific exposed values, such as the mechanism state, ion concentrations, membrane voltage, etc. +2. Right hand side of local binding in a `when` clause, tying event or post-event data to an identifier. +3. Left hand side of `effect`, corresponding to contributions of the interface to the simulation state. +4. Left hand side of `initial`, where the optional `... from` clause modifies the initial state, and also where `state` forms the left hand side of the final binding. +5. Left hand side of `evolve`, where the keyword `explicit` might be replaced with other possible descriptions, such as `implicit` for implicit ODE or DAE systems, and also where `state'` forms left hand side of the final binding. +6. Left hand side of `export`, where we have `density parameter` or `parameter`, but which could be extended to support for example the exposure of derived values to probe requests or similar. + +In addition, the set of possible interface classes can be extended. An example would be to add stateful gap junctions. + +## Default modules + +Rather than having functions such as `exp` and constant such as `π` bound by default in module scopes, built-in functions and constants could be moved to a module that is always provided by the environment. This module name can be freely chosen, but suggestions have included: `common`, `std`, `prelude`. `arblang` is another possibility. + +Importing many constants or functions from a module may be tedious: either the qualified name is used, or each must be introduced via a `def` or `let` binding. A possible extension to Arblang would be to permit `with M;` to introduce local bindings for all constants and functions defined in a module imported as _M_, in an expression scope. + +Possible example: +``` +module foo { + import common + + # Using a qualified name: + def a = common.cos(common.π/5); + + # Explicit bindiings: + def cos = common.cos; + def π = common.π; + def b = cos(π/5); + + # Using `with`: + def c = with common; cos(π/5); +} +``` + +## Alternative concentration model + +The concentration models described in [Mechanism semantics](#mechanism-semantics) are defined in terms of flow contributions, rather than in absolute concentrations, which is a departure from the NEURON NMODL approach. + +The NEURON approach has some limitations: initial concentration must be supplied by the mechanism model, not the cell description; and all contributions to concentration evolution must be combined within the one mechanism, because different concentration writing mechanisms cannot overlap. Nonetheless, the flow based description + +``` +interface concentration "CaDynamics" { + export parameter gamma: real = 0.5; + export parameter decay: time = 80 ms; + export parameter detph: length = 0.1 µm; + export parameter steady_conc: concentration = 1.0e-4 mmol/L; + + bind ca_flux = molar flux "ca"; + bind ca_conc = internal concentration "ca"; + effect internal concentration rate "ca" = -ca_flux*gamma/depth - (ca_conc-steady_conc)/decay; +} +``` + +might be represented in a direct concentration model as + +``` + export parameter gamma: real = 0.5; + export parameter decay: time = 80 ms; + export parameter detph: length = 0.1 µm; + export parameter steady_conc: concentration = 1.0e-4 mmol/L; + + initial state = steady_conc; + + bind ca_conc = state; + bind ca_flux = molar flux "ca"; + evolve state' = -ca_flux*gamma/depth - (ca_conc-steady_conc)/decay; + + effect internal concentration "ca" = ca_conc; +``` + +## Alternative function and type alias syntax + +Alternatives for function definition: + +> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? = _expression_ `;` +> +> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? { _expression_ } + +Alternative for type aliases for record types: + +> _type-alias_ ::= `record` ***symbol*** `{` _field-defn_* `}` + +## Offset units + + +Physical quantities can represent an absolute value, or a difference between absolute values. With an implicit identification between the two that takes an absolute value of zero to a zero difference, a single quantity can be used unambiguously in both contexts. + +If a quantity can be represented by different units which differ not just in scale but also in what their zero value represents as an absolute value, then only one of these units can be used to transparently represent both absolutes and differences: the other unit must be converted by scaling in a difference context, but by scaling and an additive offset in an absolute value context. + +For Arblang, this is the situation which arises if we have a unit such as degrees Celsius in addition to kelvin. Taking the zero kelvin as the zero base, a value in degrees Celsius must be translated when representing an absolute temperature, but not when representing a difference or displacement. + +Additive expressions involving quantities can be regarded as operations in affine space, with an implicit map between the vector space of translations and the affine space determined by a choice of origin. By convention, an expression _a_+_v_ in an affine space describes the action of a displacement _v_ on the point _a_, while _a_-_b_ describes the displacement _v_ that takes _b_ to _a_. Similarly, displacements can be multiplied by a scaling factor, but points in the affine space cannot. Putting this convention in place for arithmetic expressions in Arblang: + +1. _a_ + _b_ : translate _a_ to zero-based value and interpret _b_ as a displacement, e.g. 30 °C + 10 °C = 30 °C + 10 K = 303.15 K + 10 K = 313.15 K. +2. _a_ - _b_ : translate _a_ and _b_ to zero-based values and take difference, e.g. 30 °C - 10 °C = 303.15 K - 283.15 K = 20 K. +3. _a_ * _c_ : interpret _a_ as a displacement and multiply by _c_, e.g. 30 °C * 3 Hz = 30 K * 3 Hz = 90 K/s. + +There are circumstances where this might be surprising: 30 °C - 2 K won't equal 28 °C. User code that uses units such as °C would have to be careful to write e.g. 30 °C + -2 K or similar, if that is the desired interpretation. + +Implementation: a quantity value is represented not just by a magnitude and scale relative to an implicit base unit, but also with an offset. Writing the tuple as (_m_, _s_; _δ_) for magnitude, scale and offset, addition and subtraction between compatible quantities would proceed as the following, or equivalent: + +1. (_m₁_, _s₁_; _δ₁_) + (_m₂_, _s₂_; _δ₂_) = (_m₁_ + _m₂_·(_s₂_/_s₁_), _s₁_; _δ₁_) or ((_m₁_·_s₁_-_δ₁_)/_s₂_ + _m₂_, _s₂_; 0). +2. (_m₁_, _s₁_; _δ₁_) - (_m₂_, _s₂_; _δ₂_) = ((_m₁_·_s₁_-_δ₁_) - (_m₂_·_s₂_-_δ₂_), 1; 0). + +Scales themselves would comprise a power of ten exponent and, if non-metric units are accommodated, an additional normalized scaling factor. + + +## Fractional powers for quantities and units + + + +Rational powers of units and quantities can be mathematically and physically sound; in CGS electrostatic units, for example, charge has physical dimension M^(1/2)L^(3/2)T^(-1) with units 1 Fr = 1 dyn^(1/2)·cm. + +The grammar for unit and quantity expressions could be extended to permit rational powers and parentheses, and the dimensional representation of quantities can be extended to permit rational powers, not just integral powers. There is, unfortunately, no Unicode character that can semantically and visually represent a superscript slash for the purposes of writing a rational exponent as a superscript literal. + +## User-defined units + +User-defined units can be accommodated with a bit more syntax, and new identifier context. A simple proposal: + +* The units with metric prefixes defined in [Quantities](#quantities) are pre-defined identifiers in the new unit context. +* A unit definition can be made in module scope that binds an identifier in this context to a scaled combination of already defined units. +* A keyword in the definition allows that the new unit may take the standard set of metric prefixes. + +Example: +``` +unit metric dyn = 10⁻⁵ N; + +def nothing: force/length = 1 N/m - 1 kdyn/cm; +``` + +## Range-limited quantities + +The type hierarchy could be extended to accommodate quantities of limited range. In addition to the subtype relationship on record types, one would have that a limited quantity of physical dimension _D_ and range _R_ is a subtype of another quantity of dimension _D'_ and range _R'_ iff _D_=_D'_ and _R_⊂_R'_. + +Possible syntax: + +> _type-expr_ ::= `boolean` | _quantity-expr_ | _record-type-expr_ | _qualified-identifier_ +> +> _quantity-expr_ ::= _range-limit_? _quantity-term_ +> +> _range-limit_ ::= `[` _quantity-literal_ `,` _quantity-literal `]` + +(Where we add two new punctuation tokens for `[` and `]`, and for semi-bounded ranges `∞` or the contextual keyword `infinity`.) + +Example: + +``` +type branch_length = [0 mm, 20 mm] length; + +def arctanh = fn (x: [-1, 1] real) → 1/2 · ln((1+x)/(1-x)); + +def branch_scale = fn (L: branch_length) → arctanh(L/20 mm); +``` + +The term `L/20 mm` can have its type deduced to be `[0, 1] real`, which is a subtype of the `[-1, 1] real` argument to `arctanh`. + +Alternatively, as the quantity can be deduced from the literals in the interval, the syntax could simply be: + +> _quantity-expr_ ::= _range-limit_ | _quantity-term_ +> +> _range-limit_ ::= `[` _quantity-literal_ `,` _quantity-literal `]` + +making the example look like: + +``` +type branch_length = [0 mm, 20 mm]; + +def arctanh = fn (x: [-1, 1]) → 1/2 · ln((1+x)/(1-x)); + +def branch_scale = fn (L: branch_length) → arctanh(L/20 mm); +``` + +The derivative of a range-limited quantity would lose the range limit. In general, the type of an expression involving range-limited quantities would have the range deduced via interval arithmetic. + +Guarantees on run-time values falling within a range can be offered through new built-in operators for clamping a value to a range, or asserting that it lies within a range (and triggering an error state if it is not). Making up some new syntax: + +``` +# Clamp argument to non-negative real: +def f = fn (a: real) → let a = a ↓ [0, ∞]; exp(a)-1; + +# Equivalent to: +def f = fn (a: real) → let a = if a<0 then 0 else a; exp(a)-1; + +# 'Throw' an error if voltage is outside given range: +def I = fn (v: voltage) → g*((v ! [-100 mV, 100 mV]) - e); +``` + +The benefit of using a new syntactical form is to make it clear that these do not behave like functions: the type of `a ↓ [10 m, 20 m]` is `[10 m, 20 m]` not `length`, and similarly for a range assertion `a ! [10 m, 20 m]`. From ae6bf51952b0edfb16face289d0f847eb8012dc4 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Mon, 16 Aug 2021 22:10:41 +0200 Subject: [PATCH 02/11] Fix two typos --- doc/specification/language-proposal.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/specification/language-proposal.md b/doc/specification/language-proposal.md index 8b61a10..400da1a 100644 --- a/doc/specification/language-proposal.md +++ b/doc/specification/language-proposal.md @@ -689,7 +689,7 @@ The magnitude of a quantity is a member of an extended real number set _R_, wher 2. _f⁺_(⊥) = ⊥ 3. For _a_ equal to ∞, -∞, or in the complement of the domain of _f_, if lim *x*→*a* *f*(*x*) = _L_ for _L_ in ℝ or where _L_ is ∞ or -∞, then _f⁺_(_a_) = _L_ in _R_. Otherwise, _f⁺_(_a_) = ⊥. -Functions of more than one variable are extended similarly. Arithmetic operations are extended as usual to ℝ ∪ {-∞, ∞}, with the value of indeterminite forms taking the value ⊥. The value of any expression involving ⊥ is ⊥. +Functions of more than one variable are extended similarly. Arithmetic operations are extended as usual to ℝ ∪ {-∞, ∞}, with the value of indeterminate forms taking the value ⊥. The value of any expression involving ⊥ is ⊥. When interpreted or compiled into an Arbor mechanism, _R_ and operations upon it will necessarily be approximated in some manner; IEEE 754 semantics are a reasonable expectation, with NaN representing ⊥, but the interpreter or transpiler is permitted to perform algebraic simplifications including: @@ -979,7 +979,7 @@ Notes: ### Built-in functions -Arblang includse some predefined real functions, already bound in each module scope: +Arblang includes some predefined real functions, already bound in each module scope: | Function | Operation | |--------------------|---------------------------------------------------------| From 8b03e6fa15d0788f7b816e2a84fa5a86fcdc3e06 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Mon, 23 Aug 2021 12:25:32 +0200 Subject: [PATCH 03/11] Address review, discussion. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add omitted characters from _other-new-line_. * Consistently refer to non-type, non-unit expressions as 'value expressions'. * Add link to survey article on chemical reaction network theory where reaction syntax in records is discussed. * Add small example of ambiguous expression parsing leading to same semantic interpretation. * Define what is meant by an 'outer expression'. * Clarify that a _case-expr_ must have a final branch of the form `| otherwise → ...`. * Replace errant `constant` keywords with `def`. * Split when definitions into when-clauses (testing a predicate), and on-clauses (matching an event). Add an additional optional predicate to an on-clause. * Clarify that in `initial evolve for _t_ from`, _t_ must have type `time`. * Revert regime transition syntax in when-clauses and on-clauses to `regime R` from `regime = R;` on the grounds it really isn't anything like a binding. * Change when- and on-clause semantics in regimes, so that over of applicability is clear, and so that any delivered event can trigger at most one on-clause. * Clarify the points in the syntax rules where the interface extension points lie. * Fix miscellaneous small errors, bad internal links. --- doc/specification/language-proposal.md | 202 ++++++++++++------------- 1 file changed, 98 insertions(+), 104 deletions(-) diff --git a/doc/specification/language-proposal.md b/doc/specification/language-proposal.md index 400da1a..e41348b 100644 --- a/doc/specification/language-proposal.md +++ b/doc/specification/language-proposal.md @@ -6,6 +6,7 @@ The Arblang language is constrained so that every evolution and effect can be in Arblang nonetheless can also be interpreted in a purely numerical fashion in other contexts. +When Arblang source is interpreted or compiled, it is done so in an _environment_. The environment comprises state outside of any fragment of Arblang source, and determines on one hand how foreign module imports are resolved, or if there any default imports, and on the other how interfaces are presented and interpreted in the context of cell models. # Mechanism semantics @@ -153,7 +154,7 @@ A comment is introduced by `#` and then extends to the end of the line. It is th > > _cr_ ::= U+000D CARRIAGE RETURN > -> _other-new-line_ ::= U+0085 NEXT LINE | U+2028 LINE SEPARATOR | U+2029 PARAGRAPH SEPARATOR +> _other-new-line_ ::= U+000B LINE TABULATION | U+000C FORM FEED | U+0085 NEXT LINE | U+2028 LINE SEPARATOR | U+2029 PARAGRAPH SEPARATOR #### Token value @@ -505,7 +506,7 @@ A _type-expr_ is either `boolean`, a quantity term, a record type description, o > _type-expr_ ::= `boolean` | _quantity-term_ | _record-type-expr_ | _qualified-identifier_ -An expression of a given type can be constructed from type literals and constructors described below, as well as from operators acting on subexpressions (see the section _Expressions_). +An expression of a given type can be constructed from type literals and constructors described below, as well as from operators acting on subexpressions (see the section [Value expressions](#value-expressions)). In definitions of record fields, function arguments, and optionally within expressions a _type-assertion_ declares that the identifier or expression has a given type. @@ -535,7 +536,7 @@ def c: length = 3; A quantity type or record has an associated _derivative type_: -* The derivative type of a quantity type _Q_ is _Q_/ti +* The derivative type of a quantity type _Q_ is _Q_/time. * The derivative type of a record type with fields _fᵢ_ of types _Tᵢ_ is the record type with fields _fᵢ_' and types _Uᵢ_ which are the derivative types of _Tᵢ_. @@ -679,7 +680,7 @@ Arblang metric units, and their corresponding Arblang quantities: Note that the non-SI unit 'molar' is equal to 1 mol/L. -As a possible extension, Arblang might support non-zero based units such as degrees Celsius °C. Doing so, however, complicates the algebra; refer to the [appendix](#extension-offset-values-and-affine-spaces). +As a possible extension, Arblang might support non-zero based units such as degrees Celsius °C. Doing so, however, complicates the algebra; refer to the possible [Offset Units](#offset-units) extension. #### Magnitudes @@ -715,7 +716,7 @@ Correspondingly, record literals have the syntax: > _record-literal_ ::= `{` _field-defn_* `}` > -> _field-defn_ ::= ***symbol*** _type-assertion_? `=` _expression_ `;` | _reaction_ `;` +> _field-defn_ ::= ***symbol*** _type-assertion_? `=` _value-expression_ `;` | _reaction_ `;` For field definitions, if there is no type assertion given, the type of the field is deduced from the expression on the right hand side. @@ -741,25 +742,25 @@ with { a = 4; }; a # a is locally bound to the value 4 > _reaction_ ::= _right-reaction_ | _left-reaction_ | _right-left-reaction_ > -> _right-reaction_ ::= _complex_ ***right-arrow*** _complex_ `(` _expression_ `)` +> _right-reaction_ ::= _complex_ ***right-arrow*** _complex_ `(` _value-expression_ `)` > -> _left-reaction_ ::= _complex_ ***left-arrow*** _complex_ `(` _expression_ `)` +> _left-reaction_ ::= _complex_ ***left-arrow*** _complex_ `(` _value-expression_ `)` > -> _right-left-reaction_ ::= _complex_ ***right-left-arrow*** _complex_ `(` _expression_ `,` _expression_ `)` +> _right-left-reaction_ ::= _complex_ ***right-left-arrow*** _complex_ `(` _value-expression_ `,` _value-expression_ `)` > > _complex_ ::= ***empty-set*** | ***numeric-literal***? ***symbol*** ( `+` ***numeric-literal***? ***symbol*** )* -A _reaction_ clause describes a chemical reaction equation between multisets (complexes) of species. In the context of a record literal, _reaction_ clauses are translated into field definitions through a process described below. For ease of algebraic manipulation in the determination of ODE solutions and steady states, it can be useful to retain a representation of the untranslated reactions themselves together with the internal record representation. +A _reaction_ clause describes a chemical reaction equation between multisets (complexes) of species. In the context of a record literal, _reaction_ clauses are translated into field definitions through a process described below. For ease of algebraic manipulation in the determination of ODE solutions and steady states, it can be useful to retain a representation of the untranslated reactions themselves together with the internal record representation; for a nice survey on chemical reaction networks, see [Gunawardena, J. (2003) Chemical reaction network theory for in-silico biologists](http://jeremy-gunawardena.com/papers/crnt.pdf). A _complex_ is zero (represented by ***empty-set***) or more species names each represented by a ***symbol***, possibly prefixed by a positive integer coefficient, and separated by ***plus-sign***. A ***numeric-literal*** in a _complex_ term that is not a positive integer is a syntax error. The corresponding multiset comprises these species, with the coefficient determining the multiplicity. -A reaction may be a _right-reaction_, a _left-reaction_, or a _right-left-reaction_. For a _right-reaction_ or _left-reaction_, the _expression_ in parentheses is the reaction rate coefficient. A _left-reaction_ of the form `complex₁ ← complex₂ (expr)` is exactly equivalent to a _right-reaction_ of the form `complex₂ → complex₁ (expr)`. For a _right-left-reaction_, the first _expression_ in the parenthesis is the forward reaction coefficient and the second is the reverse reaction coefficient. A _right-left-reaction_ of the form `complex₁ ⇄ complex₂ (expr₁, expr₂)` is exactly equivalent to a _right-reaction_ `complex₁ → complex₂ (expr₁)` and a _left-reaction_ `complex₁ ← compex₂ (expr₂)`. +A reaction may be a _right-reaction_, a _left-reaction_, or a _right-left-reaction_. For a _right-reaction_ or _left-reaction_, the _value-expression_ in parentheses is the reaction rate coefficient. A _left-reaction_ of the form `complex₁ ← complex₂ (expr)` is exactly equivalent to a _right-reaction_ of the form `complex₂ → complex₁ (expr)`. For a _right-left-reaction_, the first _value-expression_ in the parenthesis is the forward reaction coefficient and the second is the reverse reaction coefficient. A _right-left-reaction_ of the form `complex₁ ⇄ complex₂ (expr₁, expr₂)` is exactly equivalent to a _right-reaction_ `complex₁ → complex₂ (expr₁)` and a _left-reaction_ `complex₁ ← compex₂ (expr₂)`. #### Converting reaction clauses to field definitions In a record literal, each species _α_ present in any reaction clause complex will generate a field definition for the field named _α'_. The identifier _α_ will represent a species concentration, and _α'_ its rate of change. -Consider the normalized representation of the set of reaction clauses, where each is represented by one or two right reactions of the form _Lᵢ → Rᵢ (κᵢ)_, where are _Lᵢ_ and _Rᵢ_ are complexes. Let Π*C* denote the product with multiplicity of the species terms in a complex *C*, and *μ*(*α*; *C*) the multiplicity of a species _α_ in _C_. +Consider the normalized representation of the set of reaction clauses, where each is represented by one or two right reactions of the form _Lᵢ → Rᵢ (κᵢ)_, where are _Lᵢ_ and _Rᵢ_ are complexes. Let Π*C* denote the product with multiplicity of the species terms in a complex *C*, and *μ*(*α*; *C*) the multiplicity of a species _α_ in _C_, so that e.g. Π*C* = Πα∈*C* *α*^*μ*(*α*; *C*). The expression assigned to _α'_ in its field definition is the sum of terms _κᵢ_·Π*Lᵢ*·(*μ*(*α*; *Rᵢ*) - *μ*(*α*; *Lᵢ*)) for each reaction _i_. @@ -789,23 +790,23 @@ The record literal is then algebraically equivalent to the following. A function literal gives a value of a function type. Function types have no representation in the Arblang source language, and so cannot be used in type assertions, or in function arguments. Function literals may only appear in _function-application_ expressions or as the bound value in a _let-binding_ or module _function-defn_. -> _function-literal_ ::= `fn` `(` ( _function-arg_ ( `,` _function-arg_ )* )? `)` ***right-arrow*** _expression_ | `(` _function-literal_ `)` +> _function-literal_ ::= `fn` `(` ( _function-arg_ ( `,` _function-arg_ )* )? `)` ***right-arrow*** _value-expression_ | `(` _function-literal_ `)` > > _function-arg_ ::= ***symbol*** _type-assertion_ -The identifiers introduced by _function-arg_ clauses have function scope which comprises the final defining expression. These are bound to parameter values in a function call expression (see _Expressions_ below). The final expression may be of any non-function type, but may involve identifiers bound only to: other functions, _parameter-constant_ expressions, or the function arguments. In particular, the expression may not contain identifiers bound to an external _bindable_ in an interface. +The identifiers introduced by _function-arg_ clauses have function scope which comprises the final defining expression. These are bound to parameter values in a function call expression (see [Value expressions](#value-expressions) below). The final expression may be of any non-function type, but may involve identifiers bound only to: other functions, _parameter-constant_ expressions, or the function arguments. In particular, the expression may not contain identifiers bound to an external _bindable_ in an interface. -## Expressions - +## Value Expressions + -The expression syntax below is ambiguous in that, for example, a function application or qualified identifier may be parsed as a _boolean-expr_, _algebraic-expr_, or _record-expr_. Each possible parse should be semantically equivalent. +The expression syntax below is ambiguous in that, for example, a function application or qualified identifier may be parsed as a _boolean-expr_, _algebraic-expr_, or _record-expr_. Each possible parse should be semantically equivalent, so that, for example, a qualified identifier `a.b` where `a` is a record, refers to the bound field `b` in `a` regardless of whether `a.b` was parsed as a _record-expr_ or an _algebraic-expr_. -> _expression_ ::= ( _value-binding_ | _conditional-expr_ | _boolean-expr_ | _algebraic-expr_ | _record-expr_ ) _type-assertion_? | `(` _expression_ `)` +> _value-expression_ ::= ( _value-binding_ | _conditional-expr_ | _boolean-expr_ | _algebraic-expr_ | _record-expr_ ) _type-assertion_? | `(` _value-expression_ `)` An expression with type assertion of the form `expr: T` is valid if the type of `expr` is `T` or a supertype of `T`, and ill-formed otherwise. The type of `expr: T`, if well-formed, is always the type `T`. -Each identifier or qualified identifier in an expression must be bound (in the context determined by its occurrence). In expression context, the identifier or qualified identifier may be bound to a function argument, to another expression via a value binding in an outer expression, to a record field, to a module constant or function definition, to a module parameter, or to an external quantity via an interface binding. +Each identifier or qualified identifier in an expression must be bound (in the context determined by its occurrence). In expression context, the identifier or qualified identifier may be bound to a function argument, to another expression via a value binding in an [outer expression](#outer-expression), to a record field, to a module constant or function definition, to a module parameter, or to an external quantity via an interface binding. An expression is a _constant_ expression if every identifier in the expression is bound to a module constant or another constant expression, and if every function application subexpression has a value that is a constant expression. Similarly, an expression is _parameter-constant_ if every identifier is bound to a module constant or parameter, or another parameter-constant expression, and if every function application has a value that is parameter-constant. @@ -814,15 +815,15 @@ An expression is a _constant_ expression if every identifier in the expression i > _value-binding_ ::= _let-binding_ | _with-binding_ > -> _let-binding_ ::= `let` ***symbol*** ( _type-assertion_? `=` _expression_ | `=` _function-literal_ ) `;` _expression_ +> _let-binding_ ::= `let` ***symbol*** ( _type-assertion_? `=` _value-expression_ | `=` _function-literal_ ) `;` _value-expression_ > -> _with-binding_ ::= `with` _expression_ `;` _expression_ +> _with-binding_ ::= `with` _value-expression_ `;` _value-expression_ Both `let` and `with` introduce new identifiers in expression context that can mask bindings from outer scopes. The value of the let expression `let id = expr₁; expr₂` is `expr₂` with `id` bound to `expr₁`. -The value of the where expression `where expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. +The value of the where expression `with expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. Example: @@ -832,6 +833,11 @@ with a.pos; # binds `x` to 3 m and `y` to 4 m below. a.scale*(x+y); ``` + +In a value binding `let id = expr₁; expr₂` or `with expr₁; expr₂`, `expr₂` is called the _terminal expression_, and the value binding is an _outer expression_ of `expr₂` or any of its sub-expressions. + +The value of the where expression `with expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. + As the type of a value binding is the type of its final expression, syntactic ambiguity in type assertion parsing has no semantic consequence: `let id = expr₁; expr₂: T` has the type of `expr₂: T`, which is `T` iff the type of `expr₂` is `T` or a supertype of `T` ; similarly, `(let id = expr₁; expr₂): T` has type `T` iff the type of `let id = expr₁; expr₂`, which is the type of `expr₂` is `T` or a supertype of `T`. @@ -840,15 +846,15 @@ As the type of a value binding is the type of its final expression, syntactic am > _conditional-expr_ ::= _if-expr_ | _case-expr_ > -> _if-expr_ ::= `if` _boolean-expr_ `then` _expression_ `else` _expression_ +> _if-expr_ ::= `if` _boolean-expr_ `then` _value-expression_ `else` _value-expression_ > -> _case-expr_ ::= `|` _boolean-expr_ ***right-arrow*** _expression_ )? _case-expr_ | `|` ( `otherwise` | `true` ) ***right-arrow*** _expression_ +> _case-expr_ ::= `|` _boolean-expr_ ***right-arrow*** _value-expression_ _case-expr_ | `|` ( `otherwise` | `true` ) ***right-arrow*** _value-expression_ Alternatives based on one or more conditions can be expressed with if/then/else clauses or case expressions introduced with the bar symbol. In either, the conditional expression is ill-formed if any of the _boolean-expr_ have type which is not boolean. The value of `if condition then expr₁ else expr₂` is the value of `expr₁` in the case where `condition` is true, and `expr₂` otherwise. The type of the _if-expr_ is the type of `expr₁` and `expr₂`; the expression is ill-formed if the types of `expr₁` and `expr₂` differ. -The value of `| otherwise → expr` is just the value of `expr`. `true` can be used in place of `otherwise` equivalently. For a compound _case-expr_ of the form `| condition → expr₁ case₂`, the value is `expr₁` in the case where `condition` is true, and the value of `case₂` otherwise; the expression is ill-formed if the types of `expr₁` and `case₂` differ. +The value of `| otherwise → expr` is just the value of `expr`. `true` can be used in place of `otherwise` equivalently. For a compound _case-expr_ of the form `| condition → expr₁ case₂`, the value is `expr₁` in the case where `condition` is true, and the value of `case₂` otherwise; the expression is ill-formed if the types of `expr₁` and `case₂` differ. Note that that the last clause in a _case-expr_ _must_ be of the form `| otherwise → expr` or `| true → expr`. Example: @@ -880,7 +886,7 @@ As with value bindings, there is no semantic ambiguity arising from an ambiguous > > _comparison-op_ ::= ***compare-equal*** | ***compare-not-equal*** | ***compare-less*** | ***compare-less-equal*** | ***compare-greater*** | ***compare-greater-equal*** > -> _comparison-base_ ::= _algebraic-expr_ | `(` _expression_ `)` +> _comparison-base_ ::= _algebraic-expr_ | `(` _value-expression_ `)` A compound boolean expression of the form `expr₁ or expr₂` is well defined only if the types of `expr₁` and `expr₂` are both boolean. The value is false if both `expr₁` and `expr₂` have value false, and true otherwise. The `or` operation can be considered to be left associative, but the `or` operation is both commutative and associative. @@ -904,9 +910,9 @@ A _boolean-expr_ may not involve any boolean or comparison operations, and be eq > > _algebraic-term_ ::= _algebraic-factor_ ( ( ***multiplication-dot*** | ***asterisk*** | ***division-slash*** ) _algebraic-factor_ )* > -> _algebraic-factor_ ::= _quantity-literal_ | ( ***minus-sign*** | ***square-root*** )* _algebraic-base_ _algebraic-exponent_? ) +> _algebraic-factor_ ::= _quantity-literal_ | ( ***minus-sign*** | ***square-root*** )* _algebraic-base_ _algebraic-exponent_? > -> _algebraic-base_ ::= _function-application_ | _qualified-identifier_ | _record-field-expr_ | ***numeric-literal*** | `(` _expression_ `)` +> _algebraic-base_ ::= _function-application_ | _qualified-identifier_ | _record-field-expr_ | ***numeric-literal*** | `(` _value-expression_ `)` > > _algebraic-exponent_ ::= ***superscript-literal*** | ( `^` _algebraic-factor_ )+ @@ -924,9 +930,9 @@ The square root is introduced by ***square-root*** , and an expression `√x` is The value of an additive, multiplicative or power expression follows the usual calculi of physical quantities (for one of a number of formal treatmes, see for example, P Szekeres, _The mathematical foundations of dimensional analysis and the question of fundamental units_, International Journal of Theoretical Physics 17 no. 12 (1978), doi:10.1007/BF00678423, pp. 957–974). -> _function-application_ ::= ( _qualified-identifier_ | `(` _function-literal_ `)` ) `(` ( _expression_ ( `,` _expression_ )* )? `)` +> _function-application_ ::= ( _qualified-identifier_ | `(` _function-literal_ `)` ) `(` ( _value-expression_ ( `,` _value-expression_ )* )? `)` -A _function-application_ expression is well-formed iff the function type of the _function-literal_ or the function value bound to _qualified-identifier_ is compatible with the number and types of the _expression_ clauses constituting the arguments. If the function value corresponds to the form `fn (a₁: T₁, …) → result`, then the value of the function application expression with arguments `expr₁`, … is the value of the expression `let a₁: T₁ = expr₁; … result`. +A _function-application_ expression is well-formed iff the function type of the _function-literal_ or the function value bound to _qualified-identifier_ is compatible with the number and types of the _value-expression_ clauses constituting the arguments. If the function value corresponds to the form `fn (a₁: T₁, …) → result`, then the value of the function application expression with arguments `expr₁`, … is the value of the expression `let a₁: T₁ = expr₁; … result`. ### Record expressions @@ -934,7 +940,7 @@ A _function-application_ expression is well-formed iff the function type of the > _record-expr_ ::= _record-term_ ( ***preferential-union*** _record-term_ )* > -> _record-term_ ::= _record-literal_ | _function-application_ | _qualified_identifier_ | _record-literal_ | `(` _record-expr_ `)` +> _record-term_ ::= _record-literal_ | _function-application_ | _qualified_identifier_ | `(` _record-expr_ `)` > > _record-field-expr_ ::= ( _record-literal_ | _function-application_ | `(` _record-expr_ `)` ) `.` _qualified-identifier_ @@ -1022,9 +1028,9 @@ Modules are used to collect parameters, constants, and function definitions; int > > _type-alias_ ::= `type` ***symbol*** `=` _type-expr_ `;` > -> _parameter-defn_ ::= `parameter` ***symbol*** _type-assertion_? `=` _expression_ `;` +> _parameter-defn_ ::= `parameter` ***symbol*** _type-assertion_? `=` _value-expression_ `;` > -> _constant-defn_ ::= `def` ***symbol*** _type-assertion_? `=` _expression_ `;` +> _constant-defn_ ::= `def` ***symbol*** _type-assertion_? `=` _value-expression_ `;` > > _function-defn_ ::= `def` ***symbol*** `=` _function-literal_ `;` @@ -1036,17 +1042,17 @@ Identifiers bound in module scope in one module can be used in another module or Examples: ``` module A { - constant real pi = 3; + def real pi = 3; } module X { import module A; - constant real pi = A.pi; # Also 3. + def real pi = A.pi; # Also 3. } module Y { import module A as B; - constant real pi = B.pi; # Also 3. + def real pi = B.pi; # Also 3. } ``` @@ -1076,7 +1082,7 @@ A type alias binds a non-function type to an identifier in module scope, in type Example: ``` -type foo = metre; +type foo = length; type bar = { a: time; b: foo }; # type aliases used to assert type in constant definitions: @@ -1091,7 +1097,7 @@ def s': bar' = { a' = 1.2; b' = 3.4 m/s; }; #### Parameters -A parameter definition introduces a new identifier in module scope, in expression contexts, together with a default value given by a _paramater-constant_ expression — that is, the expression can depend only upon constants and other parameters (see [Expressions](#expressions)). +A parameter definition introduces a new identifier in module scope, in expression contexts, together with a default value given by a _parameter-constant_ expression — that is, the expression can depend only upon constants and other parameters (see [Value expressions](#value-expressions)). Parameters that are exported in an interface can be bound to a user supplied value externally; they are otherwise constant. In any expression in the same module scope that uses that parameter, the value of the parameter will be the user supplied value. This applies to expressions that are bound to other parameters — for example, consider the following module and interface definition. @@ -1147,23 +1153,23 @@ def b: real = 2*sq(P); > > _bindable_ ::= `state` | `membrane` `potential` | `temperature` | (`current` `density` | `molar` `flux`) _species-name_ | (`internal` | `external`) `concentration` _species-name_ | `charge` _species-name_ > -> _initial-defn_ ::= `initial` ( `regime` `=` _qualified-identifier_ `;` )? ( _initial-post-expr_ `from` )? `state` _type-assertion_? `=` _expression_ `;` +> _initial-defn_ ::= `initial` ( `regime` _qualified-identifier_ )? ( _initial-post-expr_ `from` )? `state` _type-assertion_? `=` _value-expression_ `;` > -> _initial-post-expr_ ::= `steady` | `evolve` `for` _expression_ +> _initial-post-expr_ ::= `steady` | `evolve` `for` _value-expression_ > > _regime-defn_ ::= `regime` _identifier_ `{` ( _regime-decl_ | _regime-defn_ )* `}` > > _regime-decl_ ::= _evolve-defn_ | _when-defn_ | _effect-defn_ > -> _evolve-defn_ ::= `evolve` `explicit`? `state'` _type-assertion_? `=` _expression_ `;` +> _evolve-defn_ ::= `evolve` `explicit`? `state'` _type-assertion_? `=` _value-expression_ `;` > -> _when-defn_ ::= `when` _when-condition_ ( `regime` = _qualified-identifier_ `;` )? `state` `=` _expression_ `;` +> _when-defn_ ::= `when` _boolean-expr_ ( `regime` _qualified-identifier_ )? `state` `=` _value-expression_ `;` > -> _when-condition_ ::= _boolean-expr_ | _identifier_ _type-assertion_ = _external-event_ `;` +> _on-defn_ ::= `on` _identifier_ _type-assertion_? = _external-event_ `;` (`when` _boolean-expr_)? ( `regime` _qualified-identifier_ )? `state` `=` _value-expression_ `;` > > _external-event_ ::= `event` | `post` > -> _effect-defn_ ::= `effect` _effect_ = _expression_ `;` +> _effect-defn_ ::= `effect` _effect_ = _value-expression_ `;` > > _effect_ ::= `current` `density` _species-name_? | `molar` `flux`_species-name_ | `current` _species-name_? | `molar` `flow` `rate` _species-name_ | (`internal` | `external`) `concentration` `rate` _species-name_ > @@ -1177,6 +1183,21 @@ Definitions and bindings in interface definitions, much like in modules, have mo In the module context of an interface, the identifier `state` is already bound in an expression context to the _bindable_ `state`, and is bound to the type of the _bindable_ `state` in a type context. `state'` is the implicitly defined type alias for the derivative type of `state`. This does not preclude other bindings to the _bindable_ `state`. +#### Parameter exports + +Only parameters that are exported are visible and modifiable in cellular models. The _export-parameter-defn_ is a convenience form for defining an exporting a parameter in a single statement. +``` +interface "foo" { + parameter bar = 3 m; + export bar; + + # Equivalently: + export parameter bar = 3 m; +} +``` + +An _export-qualifier_ provides additional metadata regarding a parameter. In the initial vesion of Arblang, there is only one possible qualifier, `density`, which is applicable only for density mechanisms. The `density` qualifier indicates that mechanism effects have, or can be regarded to have, a linear dependence upon the parameter, and that consequently spatially varying values of the parameter in the model can be safely approximated by linear interpolation or averaging. + #### Initial definition The value bound to `state` in an _initial-defn_ must be of a record or quantity type. This value defines or is used to compute the initial value of the initial value problem defined by interface `evolve` and `when` definitions. The type of this value determines the type of the bindable state and the state derivative expression used in an _evolve-defn_. @@ -1185,7 +1206,7 @@ The initial regime is determined by the _regime_ clause; if none is given, the i If there is an _initial-post-expr_ `steady`, the initial state value is derived from the provided state value _s_ as a steady-state solution to the initial value problem with value _s_ at time zero and any bound interface values held constant. -If there is an _initial-post-expr_ `evolve for t` for some expression _t_, the initial state value is derived from the provided state value _s_ as the solution at time _t_ of the initial value problem with value _s_ at time zero and any bound interface values held constant. The expression _t_ must be parameter-constant. +If there is an _initial-post-expr_ `evolve for t` for some expression _t_, the initial state value is derived from the provided state value _s_ as the solution at time _t_ of the initial value problem with value _s_ at time zero and any bound interface values held constant. The expression _t_ must be parameter-constant, and be of quantity type `time`. If the interface has no _initial-defn_ at all, the initial state is defined to be the empty record `{}`. @@ -1193,7 +1214,7 @@ If the interface has no _initial-defn_ at all, the initial state is defined to b A regime defines the dynamical evolution of the mechanism state, and the effects of the mechanism state on the cellular state. There is always a top-level, unnamed regime, but more regimes can be introduced with a _regime-defn_. Associated with each regime is an evolution definition and a set of conditions that determine behaviour upon an external event or the satisfaction of some predicate. -A regime definition introduces a new regime scope: inner regimes may be given names that mask outer regime names, and regime transitions in `when` clauses can refer to regimes defined in outer scopes without further qualification. A transition can also refer to a regime in the interface by using a qualified identifier: +A regime definition introduces a new regime scope: inner regimes may be given names that mask outer regime names, and regime transitions in `when` and `on` clauses can refer to regimes defined in outer scopes without further qualification. A transition can also refer to a regime in the interface by using a qualified identifier: ``` regime A { @@ -1204,45 +1225,55 @@ regime A { regime D { # regime B is defined in outer scope. - when p(state) regime = B.C; state = f(state); + when p(state) regime B.C state = f(state); } } regime E { # regime A is defined in outer scope. - when q(state) regime = A.D; state = g(state); + when q(state) regime A.D state = g(state); } ``` If an evolution is not specified in a regime, the evolution will be that of the outer regime. Similarly, any effects defined in an outer regime will apply, if the same effect is not defined within the inner regime. The topmost unnamed regime will implicitly define an evolution if none is provided: this implicit evolution will hold the state constant over time. -Any `when` conditions defined in an outer regime, including the topmost unnamed regime, still apply in inner regimes. +Any `when` conditions or `on` conditions defined in an outer regime, including the topmost unnamed regime, are inherited by inner regimes, are tested before any additional conditions defined in the inner regime are considered. + +#### When and on semantics -#### When semantics +When clauses are triggered when the mechanism state satisfies the corresponding predicate, and an on-clause is triggered when an event of the appropriate type is delivered to the mechanism. The state is updated according to the `state = ` clause, and if a `regime` clause is present, the dynamics are shifted to the given regime. -When clauses are triggered when the mechanism state satisfies the corresponding predicate, or when an event of the appropriate type is delivered to the mechanism. The state is updated according to the `state = ` clause, and if a `regime` clause is present, the dynamics are shifted to the given regime. +Associated when- and on-clauses are considered first by scope — conditions defined in outer regimes take priority over conditions defined in an inner regime — and then by order of definition. If more than one when- or on-clause applies, they are applied in order of definition. Note that the effect of a clause may cause a transition to a regime where the set of applicable clauses differs, whence the new set is considered in its stead. -A given when clause associated with a regime _R_, with predicate _p_ applies at the point in time _t₁_ if the dynamics are in regime _R_ at _t₁_, _p_(_t₁_) is true and either _p_(_t_) is false or dynamics were in a regime _R'_ without this when clause for _t_ ∈ (_t₁_-δ, _t₁_) for some δ>0. All predicates are considered false for _t_ < 0. +A given when clause associated with a regime _R_, with predicate _p_ applies at the point in time _t₁_ if the dynamics are in regime _R_ at _t₁_, _p_(_t₁_) is true and either _p_(_t_) is false or dynamics were in a different regime _R'_ not associated with the when clause for _t_ ∈ (_t₁_-δ, _t₁_) for some δ>0. All predicates are considered false for _t_ < 0. In addition, an applicable when clause can be satisfied at most once for any point in time _t₁_. -If more than one when clause applies, they are applied in order of definition. Note that the effect of a when clause may cause a transition to a regime where the set of applicable when-clauses differs, whence the new set is considered in its stead. In any instance, no single when clause may be triggered more than once by the same event or, for predicate-based when clauses, at the same time. +If events _e₁_, _e₂_, …, _eₙ_ are delivered at time _t_, applicable on-clauses are considered in turn for _e₁_, performing any state mutations or regime transistions as required (which may change in turn the set of applicable on-clauses), then for _e₂_, and so on. Each event can trigger at most one on-clause. No when-clauses are considered at time _t_ until all events delivered at _t_ are considered. + +Consider the following situation, with the first event delivered at time _t_ with weight _w_. -Consider the following situation: ``` initial regime X state = 0; regime X { - when ev = event; state = 1; # (A) - when ev = event; regime = Y; state = 2; # (B) - when ev = event; state = 3; # (C) - when state == 4 regime = Y; state = 5; # (D) + on weight = event; when weight>2 state = 1; # (A) + on weight = event; regime = Y; state = 2; # (B) + on weight = event; state = 3; # (C) + when state == 4 regime = Y; state = 5; # (D) } regime Y { - when true regime = X; state = 4; # (E) + when true regime = X; state = 4; # (E) } ``` -On the first event, when clauses (A) and (B) will be triggered, transitioning to regime Y with state equal to 2. At this point, the event has been handled. However the clause (E) becomes applicable as soon as the evolution is considered, and state is set to 4, and regime transitions back to X. Clause (D) now applies, setting state to 5, and transitioning back to regime Y. However clause (E) has already been triggered at this time, and so cannot be applied again. +If _w_>2, clause (A) will match, and the state will be set to 1. The event is now processed, and no further on-clauses will be considered. However if _w_≤2, the following tests and actions will take place: + +1. Clause (A) will be considered and rejected, as _w_>2 is false. +2. Clause (B) will be considered and matched, setting the state to 2 and transitioning to regime Y. +3. The when-clause (E) now becomes applicable, and is satisfied, setting the state to 4 and transitioning to regime X. +4. The event has already been processed, so none of the on-clauses (A), (B), or (C) will apply. +5. The when-clause (D) is now satisfied, and the state is set to 5, and there is a transition back to regime Y. +6. The when-clause (E) has already been triggered at time _t_, and so is no longer satisfiable, leaving us in regime Y. #### Evolution @@ -1329,14 +1360,13 @@ As noted in [Mechanisms](#mechanisms), not all effects and bindings are availabl Within an interface block, there are specific points within the permitted syntax where keywords are used to refer to interface-specific values or concepts, and which constitute natural places for future extensions of the interface block to support new functionality: -1. Right hand side of `bind`, corresponding to interface-specific exposed values, such as the mechanism state, ion concentrations, membrane voltage, etc. -2. Right hand side of local binding in a `when` clause, tying event or post-event data to an identifier. -3. Left hand side of `effect`, corresponding to contributions of the interface to the simulation state. -4. Left hand side of `initial`, where the optional `... from` clause modifies the initial state, and also where `state` forms the left hand side of the final binding. -5. Left hand side of `evolve`, where the keyword `explicit` might be replaced with other possible descriptions, such as `implicit` for implicit ODE or DAE systems, and also where `state'` forms left hand side of the final binding. -6. Left hand side of `export`, where we have `density parameter` or `parameter`, but which could be extended to support for example the exposure of derived values to probe requests or similar. +1. The set of possible _interface-classes_. +2. The set of possible _bindables_ in an _external-binding_. +3. The set of possible _effects_ in an _effect-defn_. +4. The possible _initial-post-exprs_ in an _initial-defn_. +5. New evolution definitions, replacing `explicit state' = expr;` in _evolve-defn_ with other descriptions, e.g. `implicit ...` for an implicit ODE or DAE system, or a representation of a system of stochastic differential equations. +6. The set of possible _export-qualifiers_ in an _export_ or _export-parameter-defn_. -In addition, the set of possible interface classes can be extended. An example would be to add stateful gap junctions. ## Default modules @@ -1362,49 +1392,13 @@ module foo { } ``` -## Alternative concentration model - -The concentration models described in [Mechanism semantics](#mechanism-semantics) are defined in terms of flow contributions, rather than in absolute concentrations, which is a departure from the NEURON NMODL approach. - -The NEURON approach has some limitations: initial concentration must be supplied by the mechanism model, not the cell description; and all contributions to concentration evolution must be combined within the one mechanism, because different concentration writing mechanisms cannot overlap. Nonetheless, the flow based description - -``` -interface concentration "CaDynamics" { - export parameter gamma: real = 0.5; - export parameter decay: time = 80 ms; - export parameter detph: length = 0.1 µm; - export parameter steady_conc: concentration = 1.0e-4 mmol/L; - - bind ca_flux = molar flux "ca"; - bind ca_conc = internal concentration "ca"; - effect internal concentration rate "ca" = -ca_flux*gamma/depth - (ca_conc-steady_conc)/decay; -} -``` - -might be represented in a direct concentration model as - -``` - export parameter gamma: real = 0.5; - export parameter decay: time = 80 ms; - export parameter detph: length = 0.1 µm; - export parameter steady_conc: concentration = 1.0e-4 mmol/L; - - initial state = steady_conc; - - bind ca_conc = state; - bind ca_flux = molar flux "ca"; - evolve state' = -ca_flux*gamma/depth - (ca_conc-steady_conc)/decay; - - effect internal concentration "ca" = ca_conc; -``` - ## Alternative function and type alias syntax Alternatives for function definition: -> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? = _expression_ `;` +> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? = _value-expression_ `;` > -> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? { _expression_ } +> _function-defn_ ::= `function` ***symbol*** _argument-list_ _type-assertion_? { _value-expression_ } Alternative for type aliases for record types: From 5fd345038690308e1c5f697b9d021ba27cdb4479 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Mon, 23 Aug 2021 16:41:45 +0200 Subject: [PATCH 04/11] Address review comments. * Fix ytpos, thinkos. * Add on-defn to region-decls. * Use 'regime X' not 'regime = X;` syntax in example. * State that when predicates are general (i.e. need not be predicates involving just the mechanism state.) --- doc/specification/language-proposal.md | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/doc/specification/language-proposal.md b/doc/specification/language-proposal.md index e41348b..5a5b165 100644 --- a/doc/specification/language-proposal.md +++ b/doc/specification/language-proposal.md @@ -823,7 +823,7 @@ Both `let` and `with` introduce new identifiers in expression context that can m The value of the let expression `let id = expr₁; expr₂` is `expr₂` with `id` bound to `expr₁`. -The value of the where expression `with expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. +The value of the with expression `with expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. Example: @@ -836,8 +836,6 @@ a.scale*(x+y); In a value binding `let id = expr₁; expr₂` or `with expr₁; expr₂`, `expr₂` is called the _terminal expression_, and the value binding is an _outer expression_ of `expr₂` or any of its sub-expressions. -The value of the where expression `with expr₁; expr₂` is `expr₂` with the bindings `fᵢ = vᵢ` for each field `fᵢ` with value `vᵢ` in the record value of `expr₁`. If `expr₁` does not have record type, the expression is ill-formed. - As the type of a value binding is the type of its final expression, syntactic ambiguity in type assertion parsing has no semantic consequence: `let id = expr₁; expr₂: T` has the type of `expr₂: T`, which is `T` iff the type of `expr₂` is `T` or a supertype of `T` ; similarly, `(let id = expr₁; expr₂): T` has type `T` iff the type of `let id = expr₁; expr₂`, which is the type of `expr₂` is `T` or a supertype of `T`. @@ -854,7 +852,7 @@ Alternatives based on one or more conditions can be expressed with if/then/else The value of `if condition then expr₁ else expr₂` is the value of `expr₁` in the case where `condition` is true, and `expr₂` otherwise. The type of the _if-expr_ is the type of `expr₁` and `expr₂`; the expression is ill-formed if the types of `expr₁` and `expr₂` differ. -The value of `| otherwise → expr` is just the value of `expr`. `true` can be used in place of `otherwise` equivalently. For a compound _case-expr_ of the form `| condition → expr₁ case₂`, the value is `expr₁` in the case where `condition` is true, and the value of `case₂` otherwise; the expression is ill-formed if the types of `expr₁` and `case₂` differ. Note that that the last clause in a _case-expr_ _must_ be of the form `| otherwise → expr` or `| true → expr`. +The value of `| otherwise → expr` is just the value of `expr`. `true` can be used in place of `otherwise` equivalently. For a compound _case-expr_ of the form `| condition → expr₁ case₂`, the value is `expr₁` in the case where `condition` is true, and the value of `case₂` otherwise; the expression is ill-formed if the types of `expr₁` and `case₂` differ. Note that the last clause in a _case-expr_ _must_ be of the form `| otherwise → expr` or `| true → expr`. Example: @@ -1241,9 +1239,9 @@ Any `when` conditions or `on` conditions defined in an outer regime, including t #### When and on semantics -When clauses are triggered when the mechanism state satisfies the corresponding predicate, and an on-clause is triggered when an event of the appropriate type is delivered to the mechanism. The state is updated according to the `state = ` clause, and if a `regime` clause is present, the dynamics are shifted to the given regime. +When clauses are triggered when the correspnding predicate is satisfied, and an on-clause is triggered when an event of the appropriate type is delivered to the mechanism. The state is updated according to the `state = ` clause, and if a `regime` clause is present, the dynamics are shifted to the given regime. -Associated when- and on-clauses are considered first by scope — conditions defined in outer regimes take priority over conditions defined in an inner regime — and then by order of definition. If more than one when- or on-clause applies, they are applied in order of definition. Note that the effect of a clause may cause a transition to a regime where the set of applicable clauses differs, whence the new set is considered in its stead. +Associated when- and on-clauses are considered first by scope — conditions defined in outer regimes take priority over conditions defined in an inner regime — and then by order of definition. If more than one when- or on-clause applies, they are tested and applied in this order. Note that the effect of a clause may cause a transition to a regime where the set of applicable clauses differs, whence the new set is considered in its stead. A given when clause associated with a regime _R_, with predicate _p_ applies at the point in time _t₁_ if the dynamics are in regime _R_ at _t₁_, _p_(_t₁_) is true and either _p_(_t_) is false or dynamics were in a different regime _R'_ not associated with the when clause for _t_ ∈ (_t₁_-δ, _t₁_) for some δ>0. All predicates are considered false for _t_ < 0. In addition, an applicable when clause can be satisfied at most once for any point in time _t₁_. @@ -1255,14 +1253,14 @@ Consider the following situation, with the first event delivered at time _t_ wit initial regime X state = 0; regime X { - on weight = event; when weight>2 state = 1; # (A) - on weight = event; regime = Y; state = 2; # (B) - on weight = event; state = 3; # (C) - when state == 4 regime = Y; state = 5; # (D) + on weight = event; when weight>2 state = 1; # (A) + on weight = event; regime Y state = 2; # (B) + on weight = event; state = 3; # (C) + when state == 4 regime Y state = 5; # (D) } regime Y { - when true regime = X; state = 4; # (E) + when true regime X state = 4; # (E) } ``` From f3534b03766688dace3790c2fbb076d95cee80dc Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Mon, 23 Aug 2021 16:49:36 +0200 Subject: [PATCH 05/11] Fix minor typo --- doc/specification/language-proposal.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/specification/language-proposal.md b/doc/specification/language-proposal.md index 5a5b165..10e833c 100644 --- a/doc/specification/language-proposal.md +++ b/doc/specification/language-proposal.md @@ -1157,7 +1157,7 @@ def b: real = 2*sq(P); > > _regime-defn_ ::= `regime` _identifier_ `{` ( _regime-decl_ | _regime-defn_ )* `}` > -> _regime-decl_ ::= _evolve-defn_ | _when-defn_ | _effect-defn_ +> _regime-decl_ ::= _evolve-defn_ | _when-defn_ | _on-defn_ | _effect-defn_ > > _evolve-defn_ ::= `evolve` `explicit`? `state'` _type-assertion_? `=` _value-expression_ `;` > From ce33bbcd985917c3278aa9babb811577ddb310fb Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Tue, 17 Aug 2021 13:17:32 +0200 Subject: [PATCH 06/11] Add some examples. --- doc/specification/examples/ca_dynamics.al | 12 ++++ doc/specification/examples/expsyn_stdp.al | 60 ++++++++++++++++ doc/specification/examples/kd.al | 79 +++++++++++++++++++++ doc/specification/examples/na_ts.al | 56 +++++++++++++++ doc/specification/examples/nav.al | 85 +++++++++++++++++++++++ doc/specification/examples/sk.al | 18 +++++ 6 files changed, 310 insertions(+) create mode 100644 doc/specification/examples/ca_dynamics.al create mode 100644 doc/specification/examples/expsyn_stdp.al create mode 100644 doc/specification/examples/kd.al create mode 100644 doc/specification/examples/na_ts.al create mode 100644 doc/specification/examples/nav.al create mode 100644 doc/specification/examples/sk.al diff --git a/doc/specification/examples/ca_dynamics.al b/doc/specification/examples/ca_dynamics.al new file mode 100644 index 0000000..2a57e88 --- /dev/null +++ b/doc/specification/examples/ca_dynamics.al @@ -0,0 +1,12 @@ +# Adapted from Allen Institute Ca_dynamics.mod, in turn based on model of Destexhe et al. 1994. + +interface concentration "CaDynamics" { + export parameter gamma = 0.05; # Proportion of unbuffered calcium. + export parameter decay = 80 ms; # Calcium removal time constant. + export parameter minCai = 1e-4 mM; + export parameter depth = 0.1 µm; # Depth of shell. + + bind flux = molar flux "ca"; + bind cai = internal concentration "ca"; + effect molar flux rate "ca" = -gamma*flux - (cai - minCai)/decay; +} diff --git a/doc/specification/examples/expsyn_stdp.al b/doc/specification/examples/expsyn_stdp.al new file mode 100644 index 0000000..6f70a55 --- /dev/null +++ b/doc/specification/examples/expsyn_stdp.al @@ -0,0 +1,60 @@ +# Based on Arbor default/expsyn_stdp.mod + +interface discrete "expsyn_stdp" { + # A scaling factor for incoming (pre-synaptic) events is required, as the + # weight of an event is dimensionelss. + + export parameter A = 1 μS; # pre-synaptic event contribution factor + export parameter Apre = 0.01 μS; # pre-synaptic event plasticity contribution + export parameter Apost = -0.01 μS; # post-synaptic event plasticity contribution + + export parameter τ = 2 ms; # synaptic time constant + export parameter τpre = 10 ms; # pre-synaptic plasticity contribution time constant + export parameter τpost = 10 ms; # pre-synaptic plasticity contribution time constant + + export parameter gmax = 10 μS; # maximum synaptic conductance + export parameter e = 0 mV; # reversal potential + + initial state = { + g = 0 μS; + apre = 0 μS; + apost = 0 μS; + w_plastic = 0 μS; + }; + + # Expression below could have been written without the qualifying 'S.' + # by using a 'with S;' or 'with state;' instead. + + bind S = state; + + evolve state' = { + g' = -S.g/τ; + apre' = -S.apre/τpre; + apost'= -S.apost/τpost; + }; + + bind v = membrane potential; + effect current = S.g*(v - e); + + on w = event; state = { + # With proposed clamp syntax, this could be: + # g = (S.g + S.w_plastic + w·A) ↓ [0 S, gmax]; + g = max(0 μS, min(S.g + S.w_plastic + w·A, gmax)); + + apre = S.apre + Apre; + w_plastic = S.w_platic + S.apost; + }; + + on δt = post; state = { + apost = S.apost + Apost; + w_plastic = S.w_plastic + S.apre; + }; + + # The 'δt' above is ignored; it could be incorporated for an update that accounts for the + # delay between the post-synaptic event and its triggering of the `on` clause. e.g. + # + # on δt = post; state = { + # apost = S.apost + Apost·exp(-δt/τpost); + # w_plastic = S.w_plastic + S.apre·exp(δt/τpre); + # }; +} diff --git a/doc/specification/examples/kd.al b/doc/specification/examples/kd.al new file mode 100644 index 0000000..41f3e38 --- /dev/null +++ b/doc/specification/examples/kd.al @@ -0,0 +1,79 @@ +# Adapted from Allen Institute Kd.mod, in turn based on Kd model of Foust et al. 2011. +# +# Three versions, one which takes the reversal potential as a parameter, and one where it +# is computed dynamically from ion concentrations. + +module Kd { + parameter gbar = 10^-5 S/cm^2; + + def mInf = fn (v: voltage) -> + 1 - 1/(1 + exp((v + 43 mV)/8 mV)); + + def hInf = fn (v: voltage) -> + 1/(1 + exp((v + 67 mV)/7.3 mV)); + + type state = { + m: real; + h: real; + }; + + def state0 = fn (v: voltage) -> + { + m = mInf(v); + h = hInf(v); + }; + + def rate = fn (s: state, v: voltage) -> + with s; { + m' = (m - mInf(v))/1 ms; + h' = (h - hInf(v))/1500 ms; + }; + + def current = fn (s: state, v_minus_ek: voltage) -> + with s; + gbar*m*h*v_minus_ek: current/area; +} + +interface density "Kd" { + import Kd; + export density parameter Kd.gbar as gbar; + export parameter ek = -77 mV; + + bind v = membrane potential; + + initial state = Kd.state0(v); + evolve state' = Kd.rate(state, v); + effect current density "k" = Kd.current(state, v - ek); +} + +interface density "Kd_nernst" { + import Kd; + export density parameter Kd.gbar as gbar; + + bind v = membrane potential; + bind ek = nernst potential "k"; + + initial state = Kd.state0(v); + evolve state' = Kd.rate(state, v); + effect current density "k" = Kd.current(state, v - ek); +} + +# Kd_nernst is equivalent to: +# +# interface density "Kd_nernst" { +# import Kd; +# export density parameter Kd.gbar as gbar; +# +# bind v = membrane potential; +# bind T = temperature; +# bind ki = internal concentration "k"; +# bind ko = external concentration "k"; +# bind kz = charge "k"; +# +# initial state = Kd.state0(v); +# evolve state' = Kd.rate(state, v); +# effect current density "k" = +# let ek = nernst(kz, T, ki, ko); +# Kd.current(state, v - ek); +# } + diff --git a/doc/specification/examples/na_ts.al b/doc/specification/examples/na_ts.al new file mode 100644 index 0000000..46e9902 --- /dev/null +++ b/doc/specification/examples/na_ts.al @@ -0,0 +1,56 @@ +# Adapted from Allen Institute NaTs.mod, in turn based on model of Colbert and Pan 2002. + +interface density "NaTs" { + type rate = real/time; + + export density parameter gbar = 10^-5 S/cm^2; + + export parameter mαF: rate = 0.182 ms⁻¹; + export parameter mβF: rate = 0.124 ms⁻¹; + export parameter mv½: voltage = -40 mV; + export parameter mk: voltage = 6 mV; + + export parameter hαF: rate = 0.015 ms⁻¹; + export parameter hβF: rate = 0.015 ms⁻¹; + export parameter hv½: voltage = -66 mV; + export parameter hk: voltage = 6 mV; + + def rates = fn (v: voltage, T: temperature) → + let qt = 2.3^((T-296.15 K)/10 K); + + let mα = mαF·mk/exprel((mv½-v)/mk); + let mβ = mβF·mk/exprel((v-mv½)/mk); + + let hα = hαF·hk/exprel((v-hv½)/hk); + let hβ = hβF·hk/exprel((hv½-v)/hk); + + { + mi = mα/(mα + mβ); + mτ = 1/(mα + mβ)/qt; + + hi = hα/(hα + hβ); + hτ = 1/(hα + hβ)/qt; + }; + + bind T = temperature; + bind v = membrane potential; + bind ena = nernst potential "na"; + + initial state = + with rates(v, T); { + m = mi; + h = hi; + }; + + evolve state' = + with state; + with rates(v, T); { + m' = (mi - m)/mτ; + h' = (hi - h)/hτ; + }; + + effect current density "na" = + with state; + gbar·m³·h·(v - ena); +} + diff --git a/doc/specification/examples/nav.al b/doc/specification/examples/nav.al new file mode 100644 index 0000000..ea0e61c --- /dev/null +++ b/doc/specification/examples/nav.al @@ -0,0 +1,85 @@ +# Adapted from Allen Institute NaV.mod, based on kinetics +# from Carter et al. 2012 doi:10.1016/j.neuron.2012.08.033 (see Figure 7A). + +interface density "NaV" { + export density parameter g̅ = 0.015 S/cm²; + + export parameter Con = 0.01 ms⁻¹; # closed C1 → inactivated I1 transition + export parameter Coff = 40 ms⁻¹; # inactivated I1 → closed C1 transitions + export parameter Oon = 8 ms⁻¹; # open O → inactivated I6 transition + export parameter Ooff = 0.05 ms⁻¹; # inactivated I6 → open O transition + export parameter α = 400 ms⁻¹; # closed Cx right transitions (activation) + export parameter β = 12 ms⁻¹; # closed Cx left transitions (deactivation) + export parameter γ = 250 ms⁻¹; # closed → open transition + export parameter δ = 60 ms⁻¹; # open → closed transition + + export parameter a = 2.51; # factor for right Ix transitions + export parameter b = 5.32; # inverse factor for left Ix transitions + + export parameter αvdep = 24 mV; # Vdep of activation + export parameter βvdep = -24 mV; # Vdep of deactivation + + # With the proposed range-limited extension, fields below would be defined + # C1: [0, 1]; + # etc. + type state = { + C1: real; + C2: real; + C3: real; + C4: real; + C5: real; + O: real; + I1: real; + I2: real; + I3: real; + I4: real; + I5: real; + I6: real; + }; + + def kinetics = fn(s: state, v: voltage, Q: real) → + # scale rates by Q and voltage dependencies + let Con = Q·Con; + let Coff = Q·Coff; + let Oon = Q·Oon; + let Ooff = Q·Ooff; + let α = Q·α·exp(v/αvdep); + let β = Q·β·exp(v/βvdep); + let γ = Q·γ; + let δ = Q·δ; + + with s; { + C1 ⇄ C2 ( 4·α, β ); + C2 ⇄ C3 ( 3·α, 2·β ); + C3 ⇄ C4 ( 2·α, 3·β ); + C4 ⇄ C5 ( α, 4·β ); + C5 ⇄ O ( γ, δ ); + + I1 ⇄ I2 ( 4·a·α, β/b ); + I2 ⇄ I2 ( 3·a·α, 2·β/b ); + I3 ⇄ I4 ( 2·a·α, 3·β/b ); + I4 ⇄ I5 ( a·α, 4·β/b ); + I5 ⇄ I6 ( γ, δ ); + + C1 ⇄ I1 ( Con, Coff ); + C2 ⇄ I2 ( a·Con, Coff/b ); + C3 ⇄ I3 ( a²·Con, Coff/b² ); + C4 ⇄ I4 ( a³·Con, Coff/b³ ); + C5 ⇄ I5 ( a⁴·Con, Coff/b⁴ ); + O ⇄ I6 ( Oon, Ooff ); + }: state' + + bind v = membrane potential; + bind T = temperature; + bind ena = nernst potential "na"; + + def qt(T: temperature) → 2.3^((T - 310.15 K)/10 K); + + initial steady state from state = + { C1 = 1; C2 = 0; C3 = 0; C4 = 0; C5 = 0; O = 0; + I1 = 0; I2 = 0; I3 = 0; I4 = 0; I5 = 0; I6 = 0; }; + + evolve state' = kinetics(state, v, qt(T)); + + effect current density "na" = with state; g̅·O·(v - ena); +} diff --git a/doc/specification/examples/sk.al b/doc/specification/examples/sk.al new file mode 100644 index 0000000..29373db --- /dev/null +++ b/doc/specification/examples/sk.al @@ -0,0 +1,18 @@ +# Adapted from Allen Institute SK.mod, in turn based on model of Kohler et al. 1996. +# Takes fixed ek as parameter. + +interface density "SK" { + export density parameter gbar = 10^-5 S/cm^2; + export parameter zTau = 1 ms; + + def zInf(v: voltage; c: concentration) -> + | c==0 -> 0 + | otherwise -> 1/(1 + (0.00043 mM/c)^4.8); + + bind v = voltage; + bind cai = internal concentration "ca"; + + initial state = zInf(v, cai); + evolve state' = (zInf(v, cai) - state)/zTau; + effect current density "k" = gbar*state*(v - ek); +} From dcc7b323db2a6939eb0cc22c6760dd2e6a1ea856 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Mon, 30 Aug 2021 22:06:47 +0200 Subject: [PATCH 07/11] Dodge lack of min/max builtins. --- doc/specification/examples/expsyn_stdp.al | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/specification/examples/expsyn_stdp.al b/doc/specification/examples/expsyn_stdp.al index 6f70a55..294d165 100644 --- a/doc/specification/examples/expsyn_stdp.al +++ b/doc/specification/examples/expsyn_stdp.al @@ -39,7 +39,11 @@ interface discrete "expsyn_stdp" { on w = event; state = { # With proposed clamp syntax, this could be: # g = (S.g + S.w_plastic + w·A) ↓ [0 S, gmax]; - g = max(0 μS, min(S.g + S.w_plastic + w·A, gmax)); + + g = let g = S.g + S.w_plastic + w·A; + | g < 0 S → 0 S + | g > gmax → gmax + | otherwise → g; apre = S.apre + Apre; w_plastic = S.w_platic + S.apost; From 9ad09d81c5c8abf5ca49da8c030b88bb9bc2df6a Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Thu, 2 Sep 2021 11:55:32 +0200 Subject: [PATCH 08/11] Typo/copypaste fixes --- doc/specification/examples/expsyn_stdp.al | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/specification/examples/expsyn_stdp.al b/doc/specification/examples/expsyn_stdp.al index 294d165..f2ab1ff 100644 --- a/doc/specification/examples/expsyn_stdp.al +++ b/doc/specification/examples/expsyn_stdp.al @@ -10,7 +10,7 @@ interface discrete "expsyn_stdp" { export parameter τ = 2 ms; # synaptic time constant export parameter τpre = 10 ms; # pre-synaptic plasticity contribution time constant - export parameter τpost = 10 ms; # pre-synaptic plasticity contribution time constant + export parameter τpost = 10 ms; # post-synaptic plasticity contribution time constant export parameter gmax = 10 μS; # maximum synaptic conductance export parameter e = 0 mV; # reversal potential @@ -46,7 +46,7 @@ interface discrete "expsyn_stdp" { | otherwise → g; apre = S.apre + Apre; - w_plastic = S.w_platic + S.apost; + w_plastic = S.w_plastic + S.apost; }; on δt = post; state = { From 6505db9bd2b604f05482d6c1fe56319e5283b3da Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Thu, 2 Sep 2021 12:21:26 +0200 Subject: [PATCH 09/11] Adding missing ; --- doc/specification/examples/nav.al | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/specification/examples/nav.al b/doc/specification/examples/nav.al index ea0e61c..c8691fa 100644 --- a/doc/specification/examples/nav.al +++ b/doc/specification/examples/nav.al @@ -67,7 +67,7 @@ interface density "NaV" { C4 ⇄ I4 ( a³·Con, Coff/b³ ); C5 ⇄ I5 ( a⁴·Con, Coff/b⁴ ); O ⇄ I6 ( Oon, Ooff ); - }: state' + }: state'; bind v = membrane potential; bind T = temperature; From 42e938c6699e546eb282b65af089f830a827ac5d Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Thu, 2 Sep 2021 12:24:13 +0200 Subject: [PATCH 10/11] Remove errant ;s --- doc/specification/examples/kd.al | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/specification/examples/kd.al b/doc/specification/examples/kd.al index 41f3e38..ab617e9 100644 --- a/doc/specification/examples/kd.al +++ b/doc/specification/examples/kd.al @@ -35,8 +35,8 @@ module Kd { } interface density "Kd" { - import Kd; - export density parameter Kd.gbar as gbar; + import Kd + export density parameter Kd.gbar as gbar export parameter ek = -77 mV; bind v = membrane potential; @@ -47,8 +47,8 @@ interface density "Kd" { } interface density "Kd_nernst" { - import Kd; - export density parameter Kd.gbar as gbar; + import Kd + export density parameter Kd.gbar as gbar bind v = membrane potential; bind ek = nernst potential "k"; From da55fa626fb9d6bb7bf10cd73ffa008b62eed358 Mon Sep 17 00:00:00 2001 From: Sam Yates Date: Thu, 2 Sep 2021 12:24:37 +0200 Subject: [PATCH 11/11] (missed some) --- doc/specification/examples/kd.al | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/specification/examples/kd.al b/doc/specification/examples/kd.al index ab617e9..5bbb9cd 100644 --- a/doc/specification/examples/kd.al +++ b/doc/specification/examples/kd.al @@ -61,8 +61,8 @@ interface density "Kd_nernst" { # Kd_nernst is equivalent to: # # interface density "Kd_nernst" { -# import Kd; -# export density parameter Kd.gbar as gbar; +# import Kd +# export density parameter Kd.gbar as gbar # # bind v = membrane potential; # bind T = temperature;