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
{{ message }}
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
Copy file name to clipboardExpand all lines: Manual/Language/RecursiveDefs.lean
+71-5Lines changed: 71 additions & 5 deletions
Original file line number
Diff line number
Diff line change
@@ -15,38 +15,71 @@ open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
15
15
16
16
set_option maxRecDepth 1500
17
17
18
+
/-
18
19
#doc (Manual) "Recursive Definitions" =>
20
+
-/
21
+
#doc (Manual) "再帰定義（Recursive Definitions）" =>
19
22
%%%
20
23
tag := "recursive-definitions"
21
24
%%%
22
25
26
+
:::comment
23
27
Allowing arbitrary recursive function definitions would make Lean's logic inconsistent.
24
-
General recursion makes it possible to write circular proofs: "{tech}[命題]proposition $`P` is true because proposition $`P` is true".
28
+
General recursion makes it possible to write circular proofs: "{tech}[proposition] $`P` is true because proposition $`P` is true".
25
29
Outside of proofs, an infinite loop could be assigned the type {name}`Empty`, which can be used with {keywordOf Lean.Parser.Term.nomatch}`nomatch` or {name Empty.rec}`Empty.rec` to prove any theorem.
26
30
27
-
Banning recursive function definitions outright would render Lean far less useful: {tech}[帰納型]inductivetypesarekeytodefiningbothpredicatesanddata,andtheyhavearecursivestructure.
Banning recursive function definitions outright would render Lean far less useful: {tech}[inductive] types are key to defining both predicates and data, and they have a recursive structure.
28
37
Furthermore, most useful recursive functions do not threaten soundness, and infinite loops usually indicate mistakes in definitions rather than intentional behavior.
29
38
Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
30
39
While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
There are four main kinds of recursive functions that can be defined:
33
47
48
+
:::
49
+
50
+
定義できる再帰関数には主に4種類あります：
51
+
52
+
:::comment
34
53
: Structurally recursive functions
35
54
36
-
Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[添字族]indexed families are grouped together with their indices, with the whole collection considered as a unit.]
37
-
The elaborator translates the recursion into uses of the argument's {tech}[再帰子]recursor.
55
+
Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[indexed families] are grouped together with their indices, with the whole collection considered as a unit.]
56
+
The elaborator translates the recursion into uses of the argument's {tech}[recursor].
38
57
Because every type-correct use of a recursor is guaranteed to avoid infinite regress, this translation is evidence that the function terminates.
39
58
Applications of functions defined via recursors are definitionally equal to the result of the recursion, and are typically relatively efficient inside the kernel.
Many functions are also difficult to convert to structural recursion; forinstance, a function may terminate because the difference between an array index and the size of the array decreases as the index increases, but {name}`Nat.rec` isn't applicable because the index that increases is the function's argument.
44
-
Here, there is a {tech}[測度]measure of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
70
+
Here, there is a {tech}[measure] of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
45
71
In these cases, {tech}[well-founded recursion] can be used to define the function.
46
72
Well-founded recursion is a technique for systematically transforming recursive functions with a decreasing measure into recursive functions over proofs that every sequence of reductions to the measure eventually terminates at a minimum.
47
73
Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.
48
74
Even when definitional equalities exist, these functions are frequently slow to compute with because they require reducing proof terms that are often very large.
For many applications, it's not important to reason about the implementation of certain functions.
@@ -56,6 +89,13 @@ There are four main kinds of recursive functions that can be defined:
56
89
All that is required for soundness is that their return type is inhabited.
57
90
Partial functions may still be used in compiled code as usual, and they may appear in propositions and proofs; their equational theoryin Lean's logic is simply very weak.
Unsafe definitions have none of the restrictions of partial definitions.
@@ -66,18 +106,44 @@ There are four main kinds of recursive functions that can be defined:
66
106
Use this feature with care: logical soundness is not at risk, but the behavior of programs written in Lean may diverge from their verified logical models if the unsafe implementation is incorrect.
2. A termination analysis attempts to use the four techniques to justify the function to Lean's kernel.
75
132
If the definition is marked {keywordOf Lean.Parser.Command.declaration}`unsafe` or {keywordOf Lean.Parser.Command.declaration}`partial`,then that technique is used.
76
133
If an explicit {keywordOf Lean.Parser.Command.declaration}`termination_by` clause is present, then the indicated technique is the only one attempted.
77
134
If there is no such clause, then the elaborator performs a search, testing each parameter to the function as a candidate for structural recursion, and attempting to find a measure with a well-founded relation that decreases at each recursive call.
0 commit comments