Ascesis

用于分析和综合因果同步交互系统的语言。

语法

Ascesis的语法几乎完全由形式定义覆盖。主要参考是EBNF规格说明。一些关于词法分析的具体细节留给了实现笔记。还有两个主要符合的实现文件，可以作为次要参考——一个是用于句子生成的，另一个是用于解析的。

语义

目前，请参阅实现笔记。

示例

单个箭头

最简单的胖箭头规则定义了一个单箭头结构。例如，下面是规则a => b，它是Arrow结构定义的全部内容。然后，在Main结构定义的主体中实例化了Arrow结构。

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

Main结构不能显式实例化。相反，当解释包含其定义的.ces文件时执行Main的实例化。文件中定义的所有结构标识符必须是唯一的。

任何胖箭头规则都等同于由加法运算符分隔的一系列瘦箭头规则组成的规则表达式。在实现笔记中概述了胖到瘦(FIT)转换步骤。因此，上面的箭头等价于

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

如果规则表达式之间缺少加法运算符，那么它们的语法连接将被解释为对应多项式的乘法。注意，然而，当使用两个瘦箭头规则来定义单一箭头结构时，它们的乘积结果与加法结果相同。例如，下一个片段将被解释为与上面（为了简洁，这里直接在 Main 中定义）相同的箭头。

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

实际上，在这种情况下，我们得到 b • θ 作为节点 a 的效应多项式，以及 θ • a 作为节点 b 的原因多项式。

上下文

默认情况下，节点标签等于节点标识符，节点容量等于 1，所有节点到单项式的乘积度数等于 1，没有抑制剂。因此，在所有之前的例子中，这些映射都是隐式声明的。

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

以下是对单一箭头结构的参数化定义，它在上下文中实例化时提供了明确指定的节点标签和节点 a 的增加容量。

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

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

ces Main { Arrow!(a, z) }

立即和模板定义

FIXME

箭头序列

一个粗箭头规则可能由两个或更多多项式组成。例如，一个包含四个单节点多项式的粗箭头规则会产生三个箭头。

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)
}

存在四种原子规则表达式（允许在规则表达式 AST 的叶子中使用的构造）：一个单一的瘦或粗箭头规则，一个立即实例化，或一个模板实例化。

分叉

可以使用单个粗箭头规则来定义一个分叉结构。

ces Main { a => b c }

下面的每个规则表达式都是上述定义的分叉的替代定义。最终结果，即它们的乘积，也是相同的分叉。

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

选择

与分叉一样，选择结构也可以使用单个粗箭头规则来定义。

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

在箭头规则中出现的节点标识符不必是唯一的。下面是三个方向选择的有效定义。

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

以及另一个表达式，其中选择是在一组节点及其子集之间。

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

许可证

Ascesis 语言的规范在 Creative Commons Attribution 4.0 许可下发布。此实现根据 MIT 许可证发布。请阅读此存储库中的 LICENSE-CC 和 LICENSE-MIT 文件以获取更多信息。