Usage of partial functions in total function

Stream: lean4

[Param Reddy]

Hi all, I am going through FP in Lean. When reading about partial functions in https://lean-lang.org/functional_programming_in_lean/hello-world/cat.html i saw: The dump function is declared partial, because it calls itself recursively on input that is not immediately smaller than an argument. which makes sense. However, in section below it where process is defined i see: process does not need to be marked partial because it is structurally recursive. Each recursive call is provided with the tail of the input list, and all Lean lists are finite. Thus, process does not introduce any non-termination.. However this did not make sense since process in turn invokes/composed from dump so if dump does not terminate, we can not say process will terminate. So why does process not require to be marked partial? Why is partial not transitive i.e. if you call func which is not guaranteed to terminate then calling function would also not terminate right?

Would love to understand this better. Thanks for the help.

[Henrik Böving]

Partial fulfills three main jobs:

1. Allows you to define functions without termination proof
2. Makes this sound in the type system by
   a) forcing you to prove that the return type is inhabited
   b) Makes it impossible to unwrap the function definition

The last two things are what make it possible to use partial without infecting other functions. Even if you are defining a function that does not terminate using a partial one it will be impossible for you to show this because partial is completely opaque + you cannot use the return value that you get to prove false as that type must be inhabited.

[Param Reddy]

Thanks Henrik for the reply. Any reference where i can read for more details? Some things like "unwrap the function", "opaque" are not clear to me to fully appreciate understanding this.

Also Reg (1) I am guessing lean handles functions differently when it knows functions terminate. Any pointers to how lean treats functions which carry termination proof vs ones which dont?

[James Gallicchio]

Hm, I don't see the opaque keyword explained in the user manual. Here's a quick rundown:

• Definitions
  • You can define a symbol as an abbreviation for another term. So Nat.add is a definition which abbreviates a term like Nat.rec ...
  • You can "unfold" definitions, so-called "delta-reduction", where you substitute a symbol's definition for the symbol. This is the unfold (or rw or simp) tactic in Lean, and also what the typechecker does when checking if two terms are definitionally equal, and also what happens during kernel reduction.
  • Guaranteed sound: def mySymbol : MyType := ... since you provided a value of type MyType, the type is inhabited & the definition is sound
  • Computable in the kernel and the runtime (by substituting a symbol for its definition/"running the function")
• Axioms
  • An axiom is a symbol added to the context without a definition
  • This can be unsound, because for example I can say axiom proofOfFalse : False and Lean will not complain. We use axioms for e.g. Classical.choice, which we can prove at a meta-theoretic level is sound.
  • Noncomputable in both the kernel and the runtime
• Opaque definitions
  • Constants (old terminology) or "opaque definitions" are something between definitions and axioms
  • The type must be Nonempty or Inhabited, which guarantees opaque definitions are sound
  • Cannot be unfolded in proofs, and noncomputable in the kernel
  • Can be computable in the runtime. In particular, you can provide a definition that the compiler compiles to C is then executable

So, with all that said, partial is an opaque definition, which uses the potentially non-terminating body of the function as the input to the compiler. So, for partial definitions:

• the type must be Nonempty or Inhabited (try partial def whoops : False := whoops to see that error message)
• it is computable at runtime, using the potentially non-terminating function body
• it is not reducible/unfoldable/computable in the kernel. in particular this means you cannot prove anything about what the symbol evaluates to exactly. it looks like an axiom, when doing proofs.

[James Gallicchio]

I'm not sure if the manual explains the distinction between kernel reduction and runtime execution, though there are probably some good explanations of that distinction somewhere on zulip :D

[James Gallicchio]

James Gallicchio said:

Hm, I don't see the opaque keyword explained in the user manual.

(Does anyone know where I send a PR to add this to the manual?)

[James Gallicchio]

I assume it's the lean4 repo (since that seems to be where the manual source is?) but the contributing guidelines don't mention the manual from what I can see

[Param Reddy]

Thanks James. Learning more here from this discussion.
Is there a place where i can read more about kernel vs runtime? Till now I was thinking that only way to compute in lean was through beta reduction and rec reduction on inductive types. From your description seems like there are two computation engines (kernel and runtime) which can marshal data back and forth? (Guessing this is because Lean4 is also a programming language also?)

[Thea Brick]

Maybe not reading but I feel like @David Renshaw's video could be helpful? https://www.youtube.com/watch?v=FOt-GsiNJmU

[James Gallicchio]

They are essentially completely disjoint modes of computation. If I understand correctly, there's actually 3 ways to run Lean

• kernel: the soundness critical thing
• interpreter: potentially unsound, but can see through opaques, run partials, and call out to external functions implemented in C*
• compiler: same as the evaluator but AOT compiles your code down to C, which is then compiled to machine code via the LLVM toolchain
  (*not 100% confident what the interpreter can do)

[Henrik Böving]

The kernels evaluation capabilities are also more powerful than the interpreter or compiler as it is able to operate on open terms.

[Henrik Böving]

But of course interrpeter and compiler evaluation are drastically faster

[James Gallicchio]

There is a way to get back from the interpreter/compiler to the kernel, relying on the "trustCompiler" axiom, called native decide. Not sure that is particularly relevant here, though

[Param Reddy]

Henrik Böving said:

The kernels evaluation capabilities are also more powerful than the interpreter or compiler as it is able to operate on open terms.

Wont capabilities be independent? Saying that since sems like kernel will not evaluate partials while kernel can evaluate open term.

Also by open terms, I am guessing you eval 1 + x to x + 1? Am i correct in understanding this?

[Henrik Böving]

No 1+x is not reducible to x + 1 (actually im not sure withotu checking, it depends on which argument Nat.add recurses on). Open terms means that it can for example firgure out that (fun x => x + 2 + 3) is the same as (fun x => x + 5) because it can look under the binder without having an explicit value for x. So it will look just at x + 2 + 3 and figure out stuff based on that.

[Param Reddy]

Thea Brick said:

Maybe not reading but I feel like David Renshaw's video could be helpful? https://www.youtube.com/watch?v=FOt-GsiNJmU

Awesome video to understand this better. Thanks for the pointer. Looks like I keep getting more questions as i dig deeper. Why wellfounded and not direct recursion in the example. But will stop so that we don't overflow the stack for this thread.