See 1.1 Abstract Syntax Trees

see 1.1 Abstract Syntax Trees

When there are no variables, there are no assumptions, and the proof of P is a proof that Q holds for all closed ast’s.

这和 闭包 中说的闭合的集合，闭合的运算有什么关系？也就是对哪些运算闭合？

see 1.1 Abstract Syntax Trees

Let O = { Oα } be an arity-indexed family of disjoint sets of operators Oα of arity α.

see 1.1 Abstract Syntax Trees

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.

1. 元数的类型究竟是 nat ，还是一个 S* ？也就是元数带不带类型？
2. 另外这里写的 an arity has the form (s1, . . . , sn)s 一共有n+1个s放在这里，是指arity是S* × S类型的意思吗？
3. operator 的类型是 S 还是 S* × S？貌似书上是指返回值类型，感觉有些反直觉。

求更详细地定义/解释这里的 arity，arity的form， operator

注：S* 我是想表达 0到多个S的笛卡尔积，我也不知道它叫啥。