For a given set S of sorts, an arity has the form (s1, . . . , sn)s, which specifies the sort s ∈ S of an operator taking n ≥ 0 arguments, each of sort si ∈ S.
If o is an operator of arity (s1, . . . , sn)s, we say that o has sort s and has n arguments of sorts s1,...,sn.
元数的类型究竟是 nat ,还是一个 S* ?也就是元数带不带类型?
另外这里写的 an arity has the form (s1, . . . , sn)s 一共有n+1个s放在这里,是指arity是S* × S类型的意思吗?
see 1.1 Abstract Syntax Trees
求更详细地定义/解释这里的 arity,arity的form, operator
注:S* 我是想表达 0到多个S的笛卡尔积,我也不知道它叫啥。