You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For all declarations, the following preliminary checks are performed before any additional procedures specific to certain kinds of declaration:
52
+
### 公理
50
53
51
-
+ The universe parameters in the declaration's `declarationInfo`must not have duplicates. For example, a declaration `def Foo.{u, v, u} ...` would be prohibited.
+ The declaration's type must not have free variables; all variables in a "finished" declaration must correspond to a binder.
56
+
### 商类型
54
57
55
-
+ The declaration's type must be a type (`infer declarationInfo.type` must produce a `Sort`). In Lean, a declaration `def Foo : Nat.succ := ..` is not permitted; `Nat.succ` is a value, not a type.
The only checks done against axioms are those done for all declarations which ensure the `declarationInfo`passes muster. If an axiom has a valid set of universe parameters and a valid type with no free variables, it is admitted to the environment.
The `Quot` declarations are `Quot`, `Quot.mk`, `Quot.ind`, and `Quot.lift`. These declarations have prescribed types which are known to be sound within Lean's theory, so the environment's quotient declarations must match those types exactly. These types are hard-coded into kernel implementations since they are not prohibitively complex.
Definition, theorem, and opaque are interesting in that they both a type and a value. Checking these declarations involves inferring a type for the declaration's value, then asserting that the inferred type is definitionally equal to the ascribed type in the `declarationInfo`.
71
+
#### 可展性提示
68
72
69
-
In the case of a theorem, the `declarationInfo`'s type is what the user claims the type is, and therefore what the user is claiming to prove, while the value is what the user has offered as a proof of that type. Inferring the type of the received value amounts to checking what the proof is actually a proof of, and the definitional equality assertion ensures that the thing the value proves is actually what the user intended to prove.
73
+
可展性提示（Reducibility hints）包含声明应该如何展开的信息：
70
74
71
-
#### Reducibility hints
75
+
*`abbreviation` 通常总是会被展开；
76
+
*`opaque` 不会被展开；
77
+
*`regular N` 是否展开则依赖于 `N` 的值。
72
78
73
-
Reducibility hints contain information about how a declaration should be unfolded. An `abbreviation` will generally always be unfolded, `opaque` will not be unfolded, and `regular N` might be unfolded depending on the value of `N`. The `regular` reducibility hints correspond to a definition's "height", which refers to the number of declarations that definition uses to define itself. A definition `x`with a value that refers to definition `y` will have a height value greater than `y`.
Expressions will be explained in more detail below, but just to get it out in the open, the complete syntax for expressions, including the string and nat literal extensions, is as follows:
+ The expressions that have binders (lambda, pi, let, free variable) can just as easily bundle the three arguments (binder_name, binder_type, binder_style) as one argument `Binder`, where a binder is `Binder ::= Name BinderInfo Expr`. In the pseudocode that appears elsewhere I will usually treat them as though they have that property, because it's easier to read.
48
+
* 自由变量的标识符可以是唯一标识符，也可以是 deBruijn 层级。
49
49
50
-
+ Free variable identifiers can be either unique identifiers, or they can be deBruijn levels.
+ The expression type used in Lean proper also has an `mdata` constructor, which declares an expression with attached metadata. This metadata does not effect the expression's behavior in the kernel, so we do not include this constructor.
52
+
## 绑定器信息（Binder information）
53
53
54
-
55
-
## Binder information
56
-
57
-
Expressions constructed with the lambda, pi, let, and free variable constructors contain binder information, in the form of a name, a binder "style", and the binder's type. The binder's name and style are only for use by the pretty printer, and do not alter the core procedures of inference, reduction, or equality checking. In the pretty printer however, the binder style may alter the output depending on the pretty printer options. For example, the user may or may not want to display implicit or instance implicits (typeclass variables) in the output.
Free variables are used to convey information about bound variables in situations where the binder is currently unavailable. Usually this is because the kernel has traversed into the body of a binding expression, and has opted not to carry a structured context of the binding information, instead choosing to temporarily swap out the bound variable for a free variable, with the option of swapping in a new (maybe different) bound variable to reconstruct the binder. This unavailability description may sound vague, but a literal explanation that might help is that expressions are implemented as trees without any kind of parent pointer, so when we descend into child nodes (especially across function boundaries), we end up just losing sight of the elements above where we currently are in a given expression.
When an open expression is closed by reconstructing binders, the bindings may have changed, invalidating previously valid deBruijn indices. The use of unique names or deBruijn levels allow this re-closing of binders to be done in a way that compensates for any changes and ensures the new deBruijn indices of the re-bound variables are valid with respect the reconstructed telescope (see [this section](./kernel_concepts.md#implementing-free-variable-abstraction)).
Going forward, we may use some form of the term "free variable identifier" to refer to the objects in whatever scheme (unique IDs or deBruijn levels) an implementation may be using.
72
+
今后，我们可能会用“自由变量标识符”一词来泛指实现中使用的对象，无论是唯一 ID 还是 deBruijn 层级。
75
73
76
74
### `Const`
77
75
78
-
The `const`constructor is how an expression refers to another declaration in the environment, it must do so by reference.
76
+
`const`构造子表示表达式中对环境中另一个声明的引用，必须通过名称引用。
79
77
80
-
In example below, `def plusOne` creates a `Definition` declaration, which is checked, then admitted to the environment. Declarations cannot be placed directly in expressions, so when the type of `plusOne_eq_succ` invokes the previous declaration `plusOne`, it must do so by name. An expression is created: `Expr.const (plusOne, [])`, and when the kernel finds this `const` expression, it can look up the declaration referred to by name, `plusOne`, in the environment:
Expressions created with the `const` constructor also carry a list of levels which are substituted into any unfolded or inferred declarations taken from the environment by looking up the definition the `const` expression refers to. For example, inferring the type of `const List [Level.param(x)]` involves looking up the declaration for `List` in the current environment, retrieving its type and universe parameters, then substituting `x` for the universe parameter with which `List` was initially declared.
`lambda` and `pi` expressions (Lean proper uses the name `forallE` instead of `pi`) refer to function abstraction and the "forall" binder (dependent function types) respectively.
`let`is exactly what it sounds like. While `let`expressions are binders, they do not have a `BinderInfo`, their binder info is treated as `Default`.
113
+
`let`就是字面意思的 let 表达式。虽然 `let`表达式是绑定器，但它们没有显式的 `BinderInfo`，其绑定信息被视为默认（`Default`）。
110
114
111
115
```
112
116
binderName val
@@ -116,10 +120,15 @@ let (foo : Bar) := 0; foo
116
120
binderType .... body
117
121
```
118
122
119
-
120
123
### App
121
124
122
-
`app` expressions represent the application of an argument to a function. App nodes are binary (have only two children, a single function and an single argument), so `f x_0 x_1 .. x_N` is represented by `App(App(App(f, x_0), x_1)..., x_N)`, or visualized as a tree:
An exceedingly common kernel operation for manipulating expressions is folding and unfolding sequences of applications, getting `(f, [x_0, x_1, .., x_N])` from the tree structure above, or folding `f, [x_0, x_1, .., x_N]` into the tree above.
The `proj` constructor represents structure projections. Inductive types that are not recursive, have only one constructor, and have no indices can be structures.
The constructor takes a name, which is the name of the type, a natural number indicating the field being projected, and the actual structure the projection is being applied to.
169
+
会投影字段 `a`，因为它是跳过参数 `A` 和 `B` 后的第 0 个字段。
146
170
147
-
Be aware that in the kernel, projection indices are 0-based, despite being 1-based in Lean's vernacular, where 0 is the first non-parameter argument to the constructor.
For example, the kernel expression `proj Prod 0 (@Prod.mk A B a b)` would project the `a`, because it is the 0th field after skipping the parameters `A` and `B`.
173
+
---
150
174
151
-
While the behavior offered by `proj` can be accomplished by using the type's recursor, `proj` more efficiently handles frequent kernel operations.
175
+
### 字面量（Literals）
152
176
153
-
### Literals
177
+
Lean 内核可选支持任意精度的自然数（Nat）和字符串（String）字面量。
154
178
155
-
Lean's kernel optionally supports arbitrary precision Nat and String literals. As needed, the kernel can transform a nat literal `n` to `Nat.zero` or `Nat.succ m`, or convert a string literal `s` to `String.mk List.nil` or `String.mk (List.cons (Char.ofNat _) ...)`.
String literals are lazily converted to lists of characters for testing definitional equality, and when they appear as the major premise in reduction of a recursor.
182
+
字符串字面量采用惰性转换成字符列表，用于定义等价性测试以及递归器归约时的主要前提。
158
183
159
-
Nat literals are supported in the same positions as strings (definitional equality and major premises of a recursor application), but the kernel also provide support for addition, multiplication, exponentiation, subtraction, mod, division, as well as boolean equality and "less than or equal" comparisons on nat literals.
0 commit comments