#analysis #synthesis #systems #language #definition #arrow #notes

nightly ascesis

A language for analysis and synthesis of cause-effect synchronised interacting systems

6 releases

0.0.6 Apr 15, 2020
0.0.5 Jan 28, 2020
0.0.2 Nov 28, 2019
0.0.1 Jul 27, 2019

#15 in #synthesis


Used in ascetic_cli

MIT license

135KB
3.5K SLoC

Ascesis

Latest version docs Rust CC-BY-4.0 MIT

A language for analysis and synthesis of cause-effect synchronised interacting systems.

Syntax

Ascesis syntax is almost fully covered by formal definition. The primary reference is the specification in EBNF. Some details concerning lexing are left to the implementation notes. There are also two, mostly conformant implementation files, which may serve as a secondary reference — one is used for sentence generation and another for parsing.

Semantics

For now, see implementation notes.

Examples

Single arrow

The simplest fat arrow rule defines a single-arrow structure. For example, below is the rule a => b, which is the entire contents of the Arrow structure definition. The Arrow structure is in turn instantiated in the body of the Main structure definition.

ces Arrow { a => b }
ces Main { Arrow() }

The Main structure cannot be instantiated explicitly. Instead, the instantiation of Main is performed when a .ces file containing its definition is being interpreted. All structure identifiers defined in a file must be unique.

Any fat arrow rule is equivalent to a rule expression consisting of a sequence of thin arrow rules separated with (infix) addition operator. The fat-into-thin (FIT) transformation steps are sketched out in implementation notes. The arrow above is thus equivalent to

ces Arrow { { a -> b } + { b <- a } }
ces Main { Arrow() }

If the addition operator was missing between rule expressions, then their syntactic concatenation would be interpreted as multiplication of corresponding polynomials. Note, however, that when two thin arrow rules are used for defining a single-arrow structure, the result of their multiplication is the same as the result of addition. For example, next fragment will be interpreted as the same arrow as above (for brevity, here defined directly in Main),

ces Main { { a -> b } { b <- a } }

Indeed, in this case we get bθ for effect polynomial of node a, and θa for cause polynomial of node b.

Context

By default, node labels are equal to node identifiers, node capacities are equal to 1, all node-to-monomial multiplicities are equal to 1, and there are no inhibitors. Therefore, in all previous examples these mappings are declared implicitly as

vis { labels: { a: "a", b: "b" } }
caps { 1 a b }
weights { 1 a -> b, 1 b <- a }

What follows is a parameterized definition of a single-arrow structure, which is instantiated in the context providing explicitly specified node labels and increased capacity of node a.

ces Arrow(x: Node, y: Node) { x => y }

vis { labels: { a: "Source", z: "Sink" } }
caps { 3 a }

ces Main { Arrow!(a, z) }

Immediate and template definitions

FIXME

Arrow sequence

A fat arrow rule may consist of two or more polynomials. For example, a fat arrow rule with four single-node polynomials results in three arrows,

ces ThreeArrowsInARow(w: Node, x: Node, y: Node, z: Node) { w => x => y => z }

// seven arrows in a row
ces Main {
    ThreeArrowsInARow!(a, b, c, d) + { d => e } + ThreeArrowsInARow!(e, f, g, h)
}

There are four kinds of atomic rule expressions (constructs allowed in the leaves of rule expression AST): a single thin or single fat arrow rule, an immediate instantiation, or a template instantiation.

Fork

A fork structure may be defined with a single fat arrow rule,

ces Main { a => b c }

Each of the rule expressions below is an alternative definition of the same fork as defined above. The final result, their product, is the same fork as well.

ces Main {
    { b c <= a }
    { { a => b } { a => c } }
    { { a -> b c } { b c <- a } }
    { { a -> b c } + { b c <- a } }
}

Choice

Like a fork, a choice structure may be defined with a single fat arrow rule,

ces Main { a => b + c } // equivalently, b <= a => c

Node identifiers occuring in an arrow rule need not be unique. Next is a valid definition of a three-way choice,

ces Main { b <= a => c <= a => d } // equivalent to a => b + c + d

and another expression, where the choice is between a set of nodes and its subset:

ces Main { a => b c + b } // equivalent to { a => b c } + { a => b }

License

The specification of Ascesis language is licensed under the Creative Commons Attribution 4.0 license. This implementation is licensed under the MIT license. Please read the LICENSE-CC and LICENSE-MIT files in this repository for more information.

Dependencies

~8–18MB
~202K SLoC