possible semantics for partial functions

Stream: general

[Mirek Olšák]

I know that partial def is currently opaque, so it cannot be reasoned about but I was recently thinking if it could be defined. I had two ideas but I will not be surprised if it was already discussed somewhere.

[Mirek Olšák]

1. Using Acc on possible inputs, we evaluate the function if there is no infinite decreasing chain of inputs in the argument, otherwise Classical.choice.

Pros & cons:

• :check: very close to how well-founded recursion is defined
• :cross_mark: requires to know in advance which inputs we recurse on
• :cross_mark: context-sensitive, even functions that terminate in practice (e.g. because of short-circuit evaluation) could be marked as non-terminating

Code:

-- Semantics for a function defined by
partial def partFunc1_eval {In Out : Type} [Nonempty Out] {ι : In → Type}
    (rin : (input : In) → ι input → In)
    (recurse : (input : In) → (ι input → Out) → Out) : In → Out :=
  fun input ↦
    recurse input (partFunc1_eval rin recurse ∘ rin input)

-- could be:
open Classical in
noncomputable
def partFunc1 {In Out : Type} [Nonempty Out] (ι : In → Type)
    (rin : (input : In) → ι input → In)
    (recurse : (input : In) → (ι input → Out) → Out) : In → Out :=
  let r (in1 in2 : In) := ∃ x : ι in2, rin in2 x = in1
  fun input ↦
    if hcomp : Acc r input then hcomp.rec (
      fun input _ rec_out ↦
        recurse input fun x ↦ rec_out (rin input x) ⟨x, rfl⟩
    )
    else choice inferInstance

[Mirek Olšák]

2. Using uniqueness, a function will have a particular value if it is the only value that makes sense.

Pros & cons:

• :check: general, its answer will match any reasonable evaluation, even with short-circuit evaluation, recursion with higher-order function...
• :cross_mark: highly uncomputable, even if we know the partial function has a fixed value, we cannot build a computable provably terminating function calculating it

Code:

-- Defining semantics for a function defined by
partial def partFunc2_eval {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out)) :
    In → Out :=
  recurse (partFunc2_eval recurse)

/-
Predicate `Fixes recurse input output` means that `output` is the only possible
result for the given `input`.
-/
inductive Fixes {In Out : Type} (recurse : (In → Out) → (In → Out)) : In → Out → Prop
| mk
  (part : In → Option Out) -- a partial evaluation which agrees with `Fixes`
  (hpart : ∀ (in2 : In) (out2 : Out), part in2 = out2 →
    Fixes recurse in2 out2
  )
  (input : In) (out : Out) -- forces the new pair to be fixed too
  (hfix : ∀ f : In → Out,
      (∀ (in2 : In), part in2 = f in2 ∨ part in2 = none) →
      recurse f input = out
  )
    : Fixes recurse input out

open Classical in
noncomputable
def partFunc2 {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out)) :
    In → Out :=
  fun input ↦
  if h : ∃ out, Fixes recurse input out then h.choose
  else choice inferInstance

[Aaron Liu]

Mirek Olšák said:

• :cross_mark: requires to know in advance which inputs we recurse on

Can you recurse on all the inputs at once?

[Mirek Olšák]

I mean something like

def f x := ... f (f (x/2)) ...

so I don't know what the input for the outer call will be before I know how to evaluate f on x/2

[Mirek Olšák]

Actually, I like the option 2 more -- it provides enough space for people inventing computational tricks while still being consistent, and being non-computable is still much better than being undefined (opaque). Only that proving things about it is quite tricky -- I tried to prove that it is in fact unique, and I am getting lost in induction...

example {In Out : Type} [Nonempty Out] {recurse : (In → Out) → (In → Out)} (input : In)
    (out1 out2 : Out) (h1 : Fixes recurse input out1) (h2 : Fixes recurse input out2) :
    out1 = out2 := by
  classical
  induction h1 generalizing out2 with
  | mk part1 hpart1 input out1 hfix1 ih1 =>
    induction h2 generalizing out1 with
    | mk part2 hpart2 input out2 hfix2 ih2 =>
      let f (x : In) : Out :=
        if hex1 : ∃ y : Out, part1 x y then hex1.choose
        else if hex2 : ∃ y : Out, part2 x y then hex2.choose
        else Classical.choice inferInstance
      specialize hfix1 f
      specialize hfix2 f
      rw [←hfix1]
      · apply hfix2
        sorry -- the induction assumptions here might be insufficient...
      · sorry

[Mirek Olšák]

Here is a claim that I believe should be provable, and makes option 2 looking more computable. Maybe, I will get to proving it one day. It says that you can always emulate that semantics with an Acc based function as long as you modify the code of recurse a bit, and add a dependent restriction on the output.

example {In Out : Type} (recurse : (In → Out) → (In → Out))
    (input : In) (output : Out) : Fixes recurse input output ↔ (
      ∃ (r : In → In → Prop) (s : In → Out → Prop)
      (recurse' : (x : In) →
        ((x2 : In) → r x2 x → {y : Out // s x2 y}) →
        {y : Out // s x y})
        (acc : Acc r input),
      (∀ (x : In) (f : In → Out) (h : ∀ x2 : In, r x2 x → s x2 (f x2)),
        (recurse' x (fun x2 hx ↦ ⟨f x2, h x2 hx⟩)).val = recurse f x
      ) ∧
      output = (acc.rec (motive := fun x _ ↦ {y : Out // s x y})
        (fun x _ ↦ recurse' x)).val
    )
  := sorry

[Mirek Olšák]

I realized that due to lazy evaluation, there are still some cases that Option 2 does not capture, such as:

partial
def f (x : Nat) : (Nat × (Unit → Nat)) :=
  (x, fun _ : Unit ↦ (f (x+1)).1)

example : (f 5).1 = 5 := by native_decide
example : (f 5).2 () = 6 := by native_decide

[Mirek Olšák]

Deleted: doesn't work

[Mirek Olšák]

Deleted: doesn't work

[Mirek Olšák]

Ok, fully faithful semantics for partial functions doesn't exist. Trusting native_decide with partial def, leads to the existence of nonstandard natural numbers! :exploding_head: .

inductive LazyNat
| zero
| succ (k : Unit → LazyNat)
deriving Nonempty

namespace LazyNat

def toNat : LazyNat → Nat
| zero => 0
| succ k => (k ()).toNat+1

def gtNat : LazyNat → Nat → Bool
| zero, _ => false
| succ _, 0 => true
| succ a, b+1 => (a ()).gtNat b

theorem gtNat_iff {a : LazyNat} {b : Nat} : a.gtNat b ↔ a.toNat > b := by
  induction a generalizing b with
  | zero => simp [gtNat, toNat]
  | succ a ih =>
    cases b with
    | zero => simp [gtNat, toNat]
    | succ a => simp [gtNat, toNat, ih]

partial def nonstandard (_ : Unit) : LazyNat :=
  succ nonstandard

end LazyNat

def big : Nat := (LazyNat.nonstandard ()).toNat

example : big > 1 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 2 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 3 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 5 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 10 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 50 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 100 := LazyNat.gtNat_iff.mp (by native_decide)
example : big > 1000 := LazyNat.gtNat_iff.mp (by native_decide)

[Mirek Olšák]

Well, once we have a nonstandard natural number big : Nat, then this should be at least an eval-consistent interpretation of partial def , right?

noncomputable
def partFunc3 {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out)) :
    In → Out := big.iterate recurse (fun _ ↦ Classical.choice inferInstance)

Only it is quite bad for reasoning as we don't know exactly how big big is. Then I was thinking of a combination

open Classical in
noncomputable
def partFunc3' {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out)) :
    In → Out := fun input ↦
  if h : ∃ out, Fixes (big.iterate recurse) input out then h.choose
  else big.iterate recurse (fun _ ↦ choice inferInstance) input

but that feels a little overcombined...

[Robin Arnez]

There was some discussion over on #lean4 > Extrinsic termination proofs for well-founded recursion @ 💬. Also, regarding the native_decide semantics: You can only ever observe a finite part of the value, so I believe it is sound to view as having as much depth as has been observed. Also, you should probably make sure that you use opaque instead of Classical.choice since otherwise all non-terminating inputs would produce the same output.

[Mirek Olšák]

Thanks for the link, I am curious if the Myopic.Fixpoint is equivalent to my proposal. Also Mario confirmed there that the intended semantics for partial is to repeat big-times.

[Mirek Olšák]

Regarding opaque, I originally wanted it to be more explicit, ideally I would even take the default. For example, ∑' n : ℕ, 1 is also defined to be zero, and not something non-standardly large... Unfortunatelly, that wish seems inconsistent with the computation model.

[Mirek Olšák]

Myopic.Fixpoint also uses nonempty choice: https://codeberg.org/preichert/lean-extrinsic-termination-proofs/src/branch/main/Myopic/Fixpoint.lean#L33-L34

[Mirek Olšák]

Actually, I think your Terminates in that thread is straightforwardly equivalent to my Fixes, whereas the solution by @Paul Reichert is more general. But even there, there are still examples that can be computed but cannot be captured with the logic.

[Mirek Olšák]

For example this value cannot be proven with Myopic.Fixpoint (it can with native decide because it opts out for the default interpretation). On the other hand, I agree there is probably no reasonable model to handle these cases with forced non-standard values

partial def f (n : ℕ) : (ℕ × (Unit → ℕ)) :=
  (42, (fun _ ↦ (f (n+1)).2 () + 1))

#eval (f 0).1 -- 42

[Paul Reichert]

I'm not sure this is impossible for Myopic, although I haven't tried. What made you think it's impossible?

Regarding Myopic, it's very general, but is a bit dangerous. The intendes semantics I mentioned are not guaranteed by the compiler as of now (although I do not know of counterexamples), and future optimizations might violate it.

[Paul Reichert]

Mirek Olšák said:

Myopic.Fixpoint also uses nonempty choice: https://codeberg.org/preichert/lean-extrinsic-termination-proofs/src/branch/main/Myopic/Fixpoint.lean#L33-L34

This usage of choice is of a different kind. The opaque use in the fixpoint definition Robin Arnez mentioned is here, disguised as a partial function: https://codeberg.org/preichert/lean-extrinsic-termination-proofs/src/branch/main/Myopic/Fixpoint.lean#L50

[Mirek Olšák]

To my understanding, the value is chosen by choice if there is any plausible value for the value (which is in most undefined cases), and only opted out back to the opaque partial def, if the value is forced to not have any standard value.

[Mirek Olšák]

So I think in most cases where I would use choice, you would use choice too (perhaps with some value restriction).

[Mirek Olšák]

The example I wrote is a function that doesn't have any plausible value on the second coordinate.

[Mirek Olšák]

So your implementation just calls the opaque function on it, if I understand it correctly.

[Mirek Olšák]

It doesn't have any plausible value because one expansion step forces (f 0).2 () > 0, two steps force (f 0).2 () > 1, three steps force (f 0).2 () > 2 etc.

[Mirek Olšák]

Where do you see a risk of being incompatible with the compiler?

[Paul Reichert]

Mirek Olšák said:

To my understanding, the value is chosen by choice if there is any plausible value for the value (which is in most undefined cases), and only opted out back to the opaque partial def, if the value is forced to not have any standard value.

Sorry, I misunderstood your code when I wrote my answer and agree that as long as Fixes provides unique values -- which it seems that it does -- using choice here seems fine.

[Paul Reichert]

Mirek Olšák said:

It doesn't have any plausible value because one expansion step forces (f 0).2 () > 0, two steps force (f 0).2 () > 1, three steps force (f 0).2 () > 2 etc.

And I think you're right on this one, too!

[Paul Reichert]

Mirek Olšák said:

Where do you see a risk of being incompatible with the compiler?

There are some optimizations (constant folding, for example, or dead code elimination) that might eliminate infinite loops and let the function return garbage values. I'm not an expert with this (just one more reason to be very careful...), so I can't give you a very good example, but it seems possible that

• the compiler replaces an infinite loop with a garbage value
• the function terminates according to Myopic or another framework and assigns a certain known value that is different from the garbage value.

Also, note that Myopic doesn't distinguish fixpoint functionals (e.g., a function in (α → α) → α → α that is iterated in order to obtain the fixpoint) that are extensionally equal. So it is possible that the actual implementation makes a recursive call but discards its value. While this recursive call can cause infinite recursion, this useless recursive call cannot be recognized extensionally from the functional. This means that Myopic might conclude, in its own terms, that a function "terminates" while it actually doesn't. This is not a soundness problem, but it might still be undesirable.

[Matt Diamond]

those nonstandard natural numbers are really cool

it's almost like a meta-soundness bug: we have a natural number that we know will be decided as greater than every other natural number individually by native_decide, yet we can't prove this in the type theory and the existence of this number is type-theoretically impossible

[Aaron Liu]

Matt Diamond said:

we have a natural number that we know will be decided as greater than every other natural number individually by native_decide,

nit: we only know it will be decided as greater than every numeral, not "every natural number"

[Matt Diamond]

true... what's the significance of that distinction, though?

[Matt Diamond]

(not denying there is one, just want to understand your point better)

[Aaron Liu]

if we accept the existence of these nonstandard natural numbers

[Aaron Liu]

surely you aren't saying it will be decided as greater than itself

[Aaron Liu]

is that even a well-defined question anymore I don't think it terminates so it doesn't really decide the statement at all

[Matt Diamond]

surely you aren't saying it will be decided as greater than itself

of course not, I said greater than every other number (with the implication of "other than itself")

[Matt Diamond]

I'm not sure what you mean by "I don't think it terminates"

the point is that you're able to run comparisons against every other natural number using native_decide, and those decisions terminate

of course, the process of writing those down in a file doesn't terminate, but we know at a meta-level that it will always return True when asked if big is greater than some specific concrete natural number, and no natural number has that property, yet the type of big is Nat

[Matt Diamond]

I guess it's not surprising that weird things happen when you let native_decide pierce the opacity of a partial def

[Aaron Liu]

Matt Diamond said:

surely you aren't saying it will be decided as greater than itself

of course not, I said greater than every other number (with the implication of "other than itself")

surely you aren't saying it will be decided as greater than (itself + 1)

[Matt Diamond]

ah, I see your point... yes, big is provably less than big + k, so it's not greater than all other natural numbers

what's actually weird here is that this would seem to give the numerals an order type that isn't the usual $\omega$

[Aaron Liu]

that what happens with nonstandard models

[Matt Diamond]

yes but the type Nat isn't supposed to be a nonstandard model, right? like you shouldn't be able to construct big using the available type constructors... I don't even know if Nat is well-founded with big in the mix

[Aaron Liu]

Matt Diamond said:

yes but the type Nat isn't supposed to be a nonstandard model, right?

what do you mean?

[Aaron Liu]

why not?

[Matt Diamond]

how would you construct big using a finite sequence of applications of zero and succ?

[Matt Diamond]

perhaps I have a misunderstanding re: inductive types

[Matt Diamond]

also the non-well-foundedness is a bit weird (you can write a proof that big - k < big for all individual non-zero numerals k)

[Aaron Liu]

Matt Diamond said:

how would you construct big using a finite sequence of applications of zero and succ?

how would you define a nonstandard natural in PA?

[Matt Diamond]

I'm not sure how that's relevant to Lean... our version of Nat has a specific order type that I don't think these other nonstandard models share, and it's well-founded

[Aaron Liu]

PA also shows the naturals are well founded

[Aaron Liu]

well it's a bit weird though since PA is first-order

[Matt Diamond]

yes but the naturals with big are not well-founded, and Nat is well-founded

[Aaron Liu]

ok there are a few things that happen when you start to talk about proof systems

[Aaron Liu]

there are now two different versions of everything

[Matt Diamond]

okay

[Aaron Liu]

the "actual" properties of the structures and the properties you express in the formal system

[Aaron Liu]

so if I'm talking about Lean, then implicitly I'm working in another formal system that's strong enough to formalize how Lean works

[Aaron Liu]

now we know that Lean proves that Nat is well founded

[Aaron Liu]

but assuming Lean is consistent there are models of Lean where the model's Nat is not well founded

[Aaron Liu]

so what's going on here is that the statement you proved in Lean does not correspond to the property you were trying to express

[Matt Diamond]

which statement, specifically

[Aaron Liu]

the statement of WellFoundedLT Nat

[Aaron Liu]

so if Nat doesn't correspond to the actual natural numbers anymore I hope it makes sense that WellFoundedLT doesn't correspond to LT being well-founded anymore

[Matt Diamond]

okay so how do we know what model Nat is referring to at a given moment

[Aaron Liu]

from the context?

[Aaron Liu]

like just talking about Lean doesn't imply a specific model of Lean's type theory that you're using right

[Aaron Liu]

or even that you're using any model at all

[Matt Diamond]

sorry, I'm just not getting this at all... I'm just trying to point out that you can prove n < big for a seemingly infinite number of distinct numerals, and you can prove big - n < big for a seemingly infinite number of distinct numerals, and if you could prove either of these as a lemma in Lean which generalized these facts from individual instances to actual complete infinite sets of Nats, then you would be able to derive False, and that seems interesting to me

[Matt Diamond]

maybe I'm just missing some nuance here

[Matt Diamond]

I'm not saying there's an actual soundness bug, I'm just saying it's an interesting case of native_decide leading to funny results that would seem to (but not actually) contradict other facts that we can prove in Lean about the order type of Nat

in other words (adapting Mirek's code):

import Mathlib.Order.Interval.Finset.Nat

inductive LazyNat
| zero
| succ (k : Unit → LazyNat)
deriving Nonempty

namespace LazyNat

def toNat : LazyNat → Nat
| zero => 0
| succ k => (k ()).toNat+1

def gtNat : LazyNat → Nat → Bool
| zero, _ => false
| succ _, 0 => true
| succ a, b+1 => (a ()).gtNat b

theorem geNat_iff {a : LazyNat} {b : Nat} : a.gtNat b ↔ a.toNat > b := by
  induction a generalizing b with
  | zero => simp [gtNat, toNat]
  | succ a ih =>
    cases b with
    | zero => simp [gtNat, toNat]
    | succ a => simp [gtNat, toNat, ih]

partial def nonstandard (_ : Unit) : LazyNat :=
  succ nonstandard

end LazyNat

def big : Nat := (LazyNat.nonstandard ()).toNat

-- there is no infinite set where `big` is greater than all members
example : ¬∃ (S : Set Nat) (_ : S.Infinite), ∀ k ∈ S, big > k :=
by
  intro ⟨S, S_inf, hS⟩
  apply S_inf.not_bddAbove
  use big, fun x hx => (hS x hx).le

-- and yet it seems like we could assemble such a set if we kept going here!
example : big > 2 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 3 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 5 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 10 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 50 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 100 := LazyNat.geNat_iff.mp (by native_decide)
example : big > 1000 := LazyNat.geNat_iff.mp (by native_decide)

[Kevin Buzzard]

This is all a bit confusing because we seem to be conflating "in first order logic there are nonstandard models of the naturals" with "in Lean if you assume unsound axioms you can prove whatever you like".

In first order logic, you only have access to the principle of induction for predicates which you can write down in a certain first order language, and "I am a numeral" is not one of those predicates.

In Lean, which uses higher order logic, you can prove that Nat is the standard model of the naturals, and you can also use partial def and Lean.ofReduceBool and Lean.trustCompiler to prove False.

[Mirek Olšák]

I am really pleased to have sparked such a lively discussion but I had the impression that both @Aaron Liu and @Matt Diamond understand what is going on, and just argue about how to call it, and @Kevin Buzzard's comment (sorry) is rather confusing.

Kevin Buzzard said:

This is all a bit confusing because we seem to be conflating "in first order logic there are nonstandard models of the naturals" with "in Lean if you assume unsound axioms you can prove whatever you like".

In principle, nonstandard numbers do not have to be limited to a specific logic. It is a general concept that we assume an existence of a number big that is guaranteed to be bigger than all the numbers expressed with an expression 1+1+1+...+1 for any number of ones in that expression (I would call it a "standard number" some call it a "numeral", just a matter of terminology). However we are only able to only get one such inequality at a time, so this cannot introduce contradiction.

In Lean, which uses higher order logic, you can prove that Nat is the standard model of the naturals, and you can also use partial def and Lean.ofReduceBool and Lean.trustCompiler to prove False.

I think this is conflating the insane strength of Lean.ofReduceBool with what we are discussing here. You can proof False from native_decide by cheating with implemented_by, and for example defining true implemented by false. I don't think that native_decide would be considered conceptually inconsistent as long as we are very careful about all implemented_by.

On the other hand, what I showed with big is that if we want to model Lean together with a native_decide (and do not want to impose artificial hardware bounds), we have to put a nonstandard natural number into such model. So we cannot just say Type is a model of Lean's Type. We would have to do some nonstandard extension with ultraproduct, or completeness... (I expect it would probably have to go through first order)

[Kevin Buzzard]

So you're saying that "nonstandard model" makes sense outside of first order logic?

[Aaron Liu]

if it contains something nonstandard then I think it's fair to call it a nonstandard model

[Mirek Olšák]

Depending of what we call first order. For example in second order logic, we might want to model the theory's "all functions" with all functions in reality (whatever reality means), then non-standard models do not make sense. On the other hand, if we allow the model to omit some functions, we are essentially back in the first order setup, even if we have some structure on top of it.

[Kevin Buzzard]

So if I write axiom n : Nat and axiom hn : forall a, a < n then suddenly Nat becomes "nonstandard"? I thought that "nonstandard model" had a well-defined meaning in first order logic and that there was some confusion applying it in other contexts, which was why I interjected.

[Aaron Liu]

no it becomes unsound

[Kevin Buzzard]

Sure

[Kevin Buzzard]

But Nat itself didn't change, is my point

[Aaron Liu]

the difference between having one axiom forall a, a < n and an infinite family of axioms 1+1+1+1+... < n

[Aaron Liu]

Kevin Buzzard said:

But Nat itself didn't change, is my point

this statement doesn't make sense to me

[Aaron Liu]

you are implying

• Nat has a "value"
• the value of Nat depends on what axioms you have

[Kevin Buzzard]

Ok so if we add those infinitely many axioms then you're saying that it's reasonable to call Lean's nat nonstandard?

[Kevin Buzzard]

Ok then I withdraw my objection :-)

[Chris Henson]

Some of you might find this short blog post by Andrej Bauer interesting/relevant to this topic.

[Kevin Buzzard]

Aaron Liu said:

you are implying

• Nat has a "value"
• the value of Nat depends on what axioms you have

Yeah that's my model of what's going on -- Nat has a value and it's whatever vanilla Lean assigns to it. And there are statements which are true but not provable but we don't know what they are

[Kevin Buzzard]

But your second point certainly confuses me :-)

[Aaron Liu]

Kevin Buzzard said:

it's whatever vanilla Lean assigns to it.

What would that be? The GMP natural numbers?

[Kevin Buzzard]

I don't know because I've never read the source code, but not knowing is part of the fun

[Aaron Liu]

GMP is the bignum library that Lean uses

[Kevin Buzzard]

Ok well maybe some people know

[Kevin Buzzard]

All I know is that it doesn't matter

[Aaron Liu]

or do you mean all the constructible terms of type Nat quotient by "equality"

[Aaron Liu]

in that case we have numbers like docs#System.Platform.numBits which is either 32 or 64, but we don't know which one

[Kevin Buzzard]

But yeah your point about adding consistent axioms is confusing, maybe I have the wrong mental model. My mental model is "you can only prove things in lean which are true in all models of Lean's type theory, but there is a secret actual model which lean uses but which I'll only know if I read the source code, which I will never do"

[Aaron Liu]

Kevin Buzzard said:

but there is a secret actual model which lean uses but which I'll only know if I read the source code

Which source code? There's a typechecker and there's a compiler.

[Mirek Olšák]

I think we are discussing the compiler. That native_decide can introduce new axioms that should be in theory consistent but not very well known.

[Aaron Liu]

in that case the compiler does give you a model

[Henrik Böving]

Matt Diamond said:

-- and yet it seems like we could assemble such a set if we kept going here!

Keep in mind that you cannot actually keep going here, no computer can evaluate this for an arbitrarily large second value so everything is indeed still fine.

[Mirek Olšák]

Kevin Buzzard said:

So if I write axiom n : Nat and axiom hn : forall a, a < n then suddenly Nat becomes "nonstandard"? I thought that "nonstandard model" had a well-defined meaning in first order logic and that there was some confusion applying it in other contexts, which was why I interjected.

I think the difference is between a "nonstandard model", and "nonstandard numbers". While they are closely related, nonstandard numbers can be introduced to basically any logic with numbers, a nonstandard model doesn't have to exist in higher order logic if we have higher requirements about the model, but then an existence of a model is not equivalent to consistency.

[Kevin Buzzard]

Thanks for the clarification!

[James E Hanson]

Kevin Buzzard said:

So you're saying that "nonstandard model" makes sense outside of first order logic?

You can faithfully interpret Lean in a first-order theory, so the concept of non-standard models of Lean still makes sense.

[James E Hanson]

Which is basically what Mirek is saying.

[James E Hanson]

The terminology people use is 'full' or 'standard' semantics vs. Henkin semantics. Henkin semantics is basically interpreting high-order logic as a particular kind of first-order logic, and it's the only one that's actually complete for syntactic provability.

[James E Hanson]

You can't write down a computably enumerable proof system that proves all of the statements that are valid in every standard model of Lean.

[James E Hanson]

Kevin Buzzard said:

In Lean, which uses higher order logic, you can prove that Nat is the standard model of the naturals,

So on some level, you can only prove that Nat is the standard model of the naturals in Lean in the same sense that you can prove that $\mathbb{N}$ is the standard model of the naturals in ZFC. There are still arithmetically non-standard models of Lean just like how there are arithmetically non-standard models of ZFC.

[James E Hanson]

And what Mirek/Matt's example tells us is that the idealized version of Lean + propext + Classical.choice + Lean.ofReduceBool + Lean.trustCompiler actually doesn't have any standard models, which is pretty amusing to me.

[James E Hanson]

But also Lean.ofReduceBool and Lean.trustCompiler don't really operate the way an 'axiom' does in the typical sense (or even in the typical sense of the word in type theory).

[James E Hanson]

Their semantic content isn't really contained in their statements. Lean.trustCompiler is a proof of True, after all, so why is assuming it as an axiom any different from the 'axiomless' proof of True that you normally have? And likewise, the types of Lean.ofReduceBool and Lean.ofReduceNat just assert that a certain otherwise unaxiomatized constants are the identity functions on Bool and Nat, respectively. Yet somehow assuming these axioms implies something non-trivial about equality of types.

They're really more flags that tell Lean to accept certain schemas of axioms (i.e., things told to it by the compiler in a controlled way), which is why you get the LazyNat example and Violetta's observation about the cardinality model.

[James E Hanson]

Also, this is maybe a banal observation, but I find it really amusing that assuming the axioms Lean.ofReduceBool and Lean.trustCompiler produces a theorem that can only be proven if you're not on a Windows computer:

theorem not_Windows : ¬System.Platform.isWindows := by native_decide

[Mirek Olšák]

James E Hanson said:

And what Mirek/Matt's example tells us is that the idealized version of Lean + propext + Classical.choice + Lean.ofReduceBool + Lean.trustCompiler actually doesn't have any standard models, which is pretty amusing to me.

This is a funny way to state the sentiment expressed by me / Matt that although it is still consistent, it feels a bit fishy :grinning:

[James E Hanson]

Mirek Olšák said:

James E Hanson said:

And what Mirek/Matt's example tells us is that the idealized version of Lean + propext + Classical.choice + Lean.ofReduceBool + Lean.trustCompiler actually doesn't have any standard models, which is pretty amusing to me.

This is a funny way to state the sentiment expressed by me / Matt that although it is still consistent, it feels a bit fishy :grinning:

Fundamentally this example is the same as PA with a new constant $c$ and axioms asserting that $c$ is greater than any given standard natural number. This theory is conservative over PA for sentences that don't involve $c$, essentially for the same reason that Henrik pointed out. Any proof can only involve finitely many of these axioms, and so $c$ can always be soundly interpreted as some large natural number relative to a given proof. It just can't be soundly interpreted as a single natural number uniformly for all proofs.

[Matt Diamond]

Matt Diamond said:

yes but the naturals with big are not well-founded, and Nat is well-founded

@Kevin Buzzard why did I get a thumbs down here? not denying that what I said could be wrong, just curious why

[Kevin Buzzard]

It just meant "I think the naturals with big are still well-founded, because we can prove they're well-founded in Lean, and so what you're doing can't be proving that they're not well-founded".

[Aaron Liu]

there are two different version of "well-founded"

[Aaron Liu]

well-founded according to Lean and well-founded according to the meta-theory

[Matt Diamond]

yes, I know... that's why I said in my first message that this is "almost like a meta-soundness bug"... I'm aware that we're operating on multiple levels here (and I said "almost", not "actually"!)

[Aaron Liu]

ok so it becomes more difficult to tell what everyone is talking about because of that

[Matt Diamond]

I just find it so interesting that we "know" Lean's compiler can verify an arbitrarily large number of proofs about individual members of an infinite (?) type (natural numbers which can be represented by raw natural number literals) yet we can't universally quantify this fact over all members of the type within Lean.

I suppose we should expect that there are a lot of things about Lean that can't be proved within Lean, but it's fun to see a specific example. I'm curious if there are other examples of this where native_decide leads to unexpected but technically sound results.

[Aaron Liu]

Matt Diamond said:

I just find it so interesting that we "know" Lean's compiler can verify an arbitrarily large number of proofs about individual members of an infinite (?) type (natural numbers which can be represented by raw natural number literals) yet we can't universally quantify this fact over all members of the type within Lean.

You don't even have to bring in the compiler. Lean can prove the "ZFC + n inaccessible cardinals is consistent" for each numeral n (you have to use ~n-many universes in the proof) but it can't prove the statement "forall natural numbers n, ZFC + n inaccessible cardinals is consistent".

[Matt Diamond]

that's a good example!

[Matt Diamond]

that's because we can't quantify over universes, right?

[James E Hanson]

Matt Diamond said:

unexpected but technically sound results.

What counts as technically sound in your mind?

import Mathlib

axiom IntEqNat : ℤ = ℕ

theorem neg_one_eq_four_bil_ish : cast IntEqNat (-1) = 4294967295
  := by native_decide

[James E Hanson]

I don't believe this is inconsistent, but I can't figure out exactly which unsafe casts from Int to Nat native_decide counts as 'real'.

[James E Hanson]

Matt Diamond said:

that's because we can't quantify over universes, right?

Also, yes this is basically why.

[Matt Diamond]

"we can't prove False" is what I had in mind, so your example counts

[James E Hanson]

Though I suspect you can't actually prove the non-axiomatic version of this using native_decide. I.e., something of the form:

example (e : ℤ = ℕ) : cast e (-1) = 4294967295

Which, again, speaks to how Lean.trustCompiler doesn't really operate like a normal axiom.

[Matt Diamond]

I wonder if there are other fun things you can do with native_decide and partial... it seems like the trick is finding properties that can be verified via a finite process but then sneaking in non-well-founded structures within a partial function

[Violeta Hernández]

James E Hanson said:

I don't believe this is inconsistent, but I can't figure out exactly which unsafe casts from Int to Nat native_decide counts as 'real'.

As I understand it it's sound to add axioms of the form \a \simeq \b for types of the same cardinality, so under that same logic it should be sound to add axioms cast h x = e x for h : \a = \b and e : \a \simeq \b.

[James E Hanson]

Violeta Hernández said:

it should be sound to add axioms cast h x = e x for h : \a = \b and e : \a \simeq \b.

Maybe I'm misunderstanding, but isn't this just provable?

[James E Hanson]

Oh, sorry, \simeq, not \asymp.

[James E Hanson]

What do you mean by \simeq?

[Violeta Hernández]

docs#Equiv
sorry, currently on mobile

[James E Hanson]

I'm confused by your statement then. If two types A and B have the same cardinality, then A ≃ B should be a provable theorem. Why would you need to add it as an axiom?

[Mirek Olšák]

James E Hanson said:

Matt Diamond said:

unexpected but technically sound results.

What counts as technically sound in your mind?

import Mathlib

axiom IntEqNat : ℤ = ℕ

theorem neg_one_eq_four_bil_ish : cast IntEqNat (-1) = 4294967295
  := by native_decide

Axiomatically adding ℤ = ℕ is literally inconsistent with native_decide, I thought that was Violeta's example.

[Mirek Olšák]

Matt Diamond said:

I wonder if there are other fun things you can do with native_decide and partial... it seems like the trick is finding properties that can be verified via a finite process but then sneaking in non-well-founded structures within a partial function

Not really, as I mentioned, once you have a non-standard natural number big, you could define the actual meaning of partial def as

partial def pf {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out))
    (input : In) : Out :=
  recurse (pf recurse) input

@[implemented_by pf]
def f {In Out : Type} [Nonempty Out] (recurse : (In → Out) → (In → Out)) :
    In → Out :=
  big.repeat recurse (fun _ ↦ Classical.ofNonempty)

[Mirek Olšák]

Mirek Olšák said:

Axiomatically adding ℤ = ℕ is literally inconsistent with native_decide, I thought that was Violeta's example.

I see, that example was a bit different, well nevertheless...

axiom IntEqNat : Int = Nat

theorem neg_one_eq_four_bil_ish : cast IntEqNat (-1) = 4294967295
  := by native_decide
theorem four_bil_ish_eq_four_bil_ish : (cast IntEqNat 4294967295) - 4294967294 = 1
  := by native_decide

theorem add_of_sub {a b c : Nat} (h2 : c ≠ 0) (h1 : a - b = c) : a = c + b := by
  refine (Nat.sub_eq_iff_eq_add ?_).mp h1
  apply Decidable.not_not.mp
  intro le_ab
  simp only [Nat.not_le] at le_ab
  replace le_ab := Nat.le_of_succ_le le_ab
  rw [Nat.sub_eq_zero_of_le le_ab] at h1
  exact h2 h1.symm

theorem contradiction : False := by
  have := add_of_sub Nat.one_ne_zero four_bil_ish_eq_four_bil_ish
  simp only [Nat.reduceAdd] at this
  rw [←neg_one_eq_four_bil_ish] at this
  have := congrArg (cast IntEqNat.symm) this
  simp at this

/--
info: 'contradiction' depends on axioms: [IntEqNat, propext, Lean.ofReduceBool, Lean.trustCompiler]
-/
#guard_msgs in
#print axioms contradiction

[Mirek Olšák]

I don't know what exactly is going on but my understanding is that the compiler is not really built for Int = Nat

example : (cast IntEqNat 4294967295) - 1 = 4294967294 := by native_decide
example : ¬ (cast IntEqNat 4294967295) = 4294967295 := by native_decide

[Kevin Buzzard]

So this is a proof that the compiler is not using the cardinality model :-)

[James E Hanson]

I wouldn't say it's really accurate to say the compiler is 'using a particular model' at all.

[James E Hanson]

Mirek Olšák said:

I see, that example was a bit different, well nevertheless...

I wonder why

example : cast IntEqNat 4294967295 ≠ 4294967295 := by native_decide

works then. I know that this isn't surprising logically, but on an implementation level I'm curious.

[Robin Arnez]

The left-hand side is the GMP value 4294967295 (encoded as a pointer) and the right-hand side is the scalar 4294967295 (encoded as 4294967295*2 + 1). In other words, this breaks the assumption that GMP values are always >= USize.size / 2. Also funnily enough, on 32-bit builds both of these would be represented as GMP so the equality would actually hold.

[Matt Diamond]

@Mirek Olšák you can also create "infinite" Lists/Arrays with a length greater than any specific numeral:

import Mathlib.Data.List.Basic

inductive LazyList (α : Type)
| nil
| cons (head : α) (tail : Unit → LazyList α)
deriving Nonempty

variable {α β : Type}

namespace LazyList

def toList : LazyList α → List α
| nil => []
| cons h t => h :: (t ()).toList

def longerThanList : LazyList α → List β → Bool
| nil, _ => false
| cons _ _, [] => true
| cons _ t, _ :: t' => (t ()).longerThanList t'

theorem longerThanList_iff {a : LazyList α} {b : List β} : a.longerThanList b ↔ a.toList.length > b.length := by
  induction a generalizing b with
  | nil => simp [longerThanList, toList]
  | cons h t IH =>
    cases b with
    | nil => simp [longerThanList, toList]
    | cons h t => simp [longerThanList, toList, IH]

theorem longerThan {a : LazyList α} {k : ℕ} : a.longerThanList (List.range k) → a.toList.length > k :=
by simp [LazyList.longerThanList_iff]

partial def infiniteList (a : α) (_ : Unit) : LazyList α :=
  cons a (infiniteList a)

end LazyList

def longList : List Nat := (LazyList.infiniteList 0 ()).toList
def longArray : Array Nat := longList.toArray

example : longList.length > 10000 := LazyList.longerThan (by native_decide)
example : longArray.size > 10000 := LazyList.longerThan (by native_decide)

[Matt Diamond]

(obviously not useful in any way, but still kind of amusing)

[Mario Carneiro]

James E Hanson said:

Matt Diamond said:

unexpected but technically sound results.

What counts as technically sound in your mind?

import Mathlib

axiom IntEqNat : ℤ = ℕ

theorem neg_one_eq_four_bil_ish : cast IntEqNat (-1) = 4294967295
  := by native_decide

This is one of a family of very bad things you can observe using axiomatized type casts. It's really just an unsafe cast with extra steps. Try saying that Nat = String for more fun

[Mirek Olšák]

Mario Carneiro said:

Try saying that Nat = String for more fun

I hoped for fun, and my Lean just crashed...

[James E Hanson]

Robin Arnez said:

The left-hand side is the GMP value 4294967295 (encoded as a pointer) and the right-hand side is the scalar 4294967295 (encoded as 4294967295*2 + 1). In other words, this breaks the assumption that GMP values are always >= USize.size / 2. Also funnily enough, on 32-bit builds both of these would be represented as GMP so the equality would actually hold.

Thanks but why then does

#eval (unsafeCast 4294967295 : Nat) = (4294967295 : Nat)

evaluate to true? Why isn't casting with an axiomatic equality the same as unsafe casting at runtime? (I checked and #eval (cast IntEqNat 4294967295 : Nat) = 4294967295 evaluates to false.)

[Aaron Liu]

Casting a Nat to a Nat I wouldn't expect any difficulties

[James E Hanson]

Oh duh.

[Mirek Olšák]

Matt Diamond said:

Mirek Olšák you can also create "infinite" Lists/Arrays with a length greater than any specific numeral:

Sure, all I meant is that you can already have this kind of fun just with a nonstandard natural number. You can build for example

def nonstandardList : List ℕ := List.range big
def nonstandardFinset : Finset ℤ := .Icc (-big) big
...

[James E Hanson]

You can also just do a typical kind of lazy list example.

partial def lazyList : Unit → List Nat := fun _ ↦ (0 :: (lazyList ()))

[James E Hanson]

Oh sorry, Matt already said that.

[Matt Diamond]

oh right, that's true... so you basically get all of these other objects for free, in a sense

[Mario Carneiro]

I think you don't need nonstandard models to make sense of this behavior. As others have mentioned up-thread, you can't even prove big is very large, let alone nonstandard. I'm pretty sure you can literally just say that big = 100000 or so and you would have difficulty showing some behavior of native_decide inconsistent with this

[Mario Carneiro]

and the underlying model here is to have partial def be defined by iterating the function big many times on the default value supplied by the instance

[Mario Carneiro]

Note that this limits some compilation tricks. I tried for a while to get a contradiction by evaluating nonstandard () and some of its unfoldings and note that the result is pointer-equal, but it seems the semantics of the thunks created are such that each unfolding produces a new object

[Mario Carneiro]

If it was possible to have recursion between a value and a function I think you could get an inconsistency, e.g.

mutual
partial def nonstandard : LazyNat := succ nonstandardF
partial def nonstandardF (_ : Unit) : LazyNat := nonstandard
end

[Matt Diamond]

is the idea here that the value of big is whatever the maximum recursion depth is + 1?

[Mario Carneiro]

yes

[Mirek Olšák]

Mario Carneiro said:

I think you don't need nonstandard models to make sense of this behavior. As others have mentioned up-thread, you can't even prove big is very large, let alone nonstandard. I'm pretty sure you can literally just say that big = 100000 or so and you would have difficulty showing some behavior of native_decide inconsistent with this

Having difficulty is somewhat different from impossibility. Imagine you eventually get to implement what it means to be a proof with native_decide & partial def in Lean4Lean. Would you hardcode a limit on how many steps the evaluation can take? If so, why not a hard limit on the size of the proof term itself? (it also cannot be too large in practice)

[Mario Carneiro]

as long as big is larger than the largest recursion depth in any observed native_decide computation you are ok

[Mario Carneiro]

@Mirek Olšák yes that's exactly what I'd do

[Mario Carneiro]

it's easy enough to have a limit which is so large that you don't even need to keep track of it because the machine will break first

[Mario Carneiro]

Mirek Olšák said:

If so, why not a hard limit on the size of the proof term itself? (it also cannot be too large in practice)

There is already such a limit :grinning_face_with_smiling_eyes:

[Mario Carneiro]

recall some discussion previously about unsoundness in the kernel due to depth overflow

[Mirek Olšák]

I would argue that proofs without a hard limit have nicer theoretical properties, but sure, not believing in the existence of the number 10^100 is also a valid philosophy...

[Mirek Olšák]

I would prefer fixing the soundness bug rather than plugging hardware constraints into proof theory but hard to convince the developers, I guess...

[Mario Carneiro]

It's not that the proof theory needs a hard limit, the implementation needs a limit

[Mario Carneiro]

same here, it's a limitation on the maximum recursion depth of an observed native_decide computation

[Mario Carneiro]

Mirek Olšák said:

I would prefer fixing the soundness bug rather than plugging hardware constraints into proof theory but hard to convince the developers, I guess...

what soundness bug? My point is that not only can you model this with a nonstandard model, you can do it with a standard model too, so obviously it's not unsound

[Mirek Olšák]

I meant the bug you mentioned that panics if the recursion depth is too high.

[Mario Carneiro]

well there is no proposal for fixing that which will make the limit magically disappear, it's just a question of what happens when you reach the limit

[Mario Carneiro]

ultimately implementation limits are a fact of life

[Mirek Olšák]

Mario Carneiro said:

It's not that the proof theory needs a hard limit, the implementation needs a limit

Depending on what you mean by implementation. If running on a physical machine, then yes, there are numbers you have no chance of evaluating in practice. On the other hand, many languages (including Lean) abstract the physical limit away, and let you operate seemingly arbitrary values even if they don't fit a physical machine. So sure, you cannot evaluate arbitrary program on a physical machine, but you can still define what it means to be a result of an unbounded computation.

[Mario Carneiro]

you only get native_decide "axioms" from real hardware computations

[Mario Carneiro]

and those have limits that you can work out in advance

[Kyle Miller]

My understanding of Mirek's example is that laziness means that LazyNat at runtime, when restricted only to those terminating thunks, is a coinductive type instead. The coinductive natural number type (CoNat) consists of all the elements of Nat along with an additional infinity element ("nonstandard").

I don't think this counts as a nonstandard model of Nat, since it wouldn't have the same induction principle as Nat.

[Mario Carneiro]

James E Hanson said:

And what Mirek/Matt's example tells us is that the idealized version of Lean + propext + Classical.choice + Lean.ofReduceBool + Lean.trustCompiler actually doesn't have any standard models, which is pretty amusing to me.

And just to clarify on this point, the "axiom" isn't Lean.ofReduceBool or Lean.trustCompiler, it's the axiom scheme that says that Lean.reduceBool foo reduces to true or false depending on whether the IR compiled from foo evaluates to true or false in the interpreter

[Mirek Olšák]

Mario Carneiro said:

you only get native_decide "axioms" from real hardware computations

I don't see why this is a meaningful constraint. In the same logic, you should not claim that the theory of Lean is equivalent to ZFC + {"there are n inaccessibles" for n in N} but rather that it is equivalent to ZFC + {"there are n inaccessibles" for n which fits into a physical machine}

[Mario Carneiro]

@Kyle Miller the problem is that Nat is still inductive notwithstanding the fact that it has infinite elements

[Mario Carneiro]

that's why it looks nonstandard-ish

[Mario Carneiro]

The question is how you define the lean axiomatic system @Mirek Olšák . If you want to include native_decide "axioms" you need a model for how interpreter evaluation works and this is intensely machine-specific in a variety of ways

[Mario Carneiro]

so it's not actually that weird that a machine-specific limit could pop up there

[Mirek Olšák]

Kyle Miller said:

My understanding of Mirek's example is that laziness means that LazyNat at runtime, when restricted only to those terminating thunks, is a coinductive type instead. The coinductive natural number type (CoNat) consists of all the elements of Nat along with an additional infinity element ("nonstandard").

I don't think this counts as a nonstandard model of Nat, since it wouldn't have the same induction principle as Nat.

Just to clarify my example, LazyNat is just a helper tool, the main point was the construction of big : Nat which is larger than any number of steps that can be performed by native_decide

[Kyle Miller]

I get that @Mirek Olšák, it serves its purpose. Your element is also a perfectly defined element of the coinductive type.

I just think it's worth distinguishing between nonstandard peano arithmetic and whatever captures what the runtime LazyNat type represents. Like, big + 1 = big is true, if we could somehow evaluate its truth at runtime, which violates no-confusion for inductive type constructors. In nonstandard PA, there's no such n such that n + 1 = n, right?

[Mario Carneiro]

I think it makes more sense to just stick with LazyNat because it has the laziness you need to implement terminating computations. As soon as you make big : Nat you have a value that won't be used in any terminating native_decide computation

[Mario Carneiro]

But LazyNat is not coinductive, it's provably isomorphic to Nat

[Kyle Miller]

Mario, I'm saying the runtime type is equivalent to CoNat (with the proviso I mentioned that you only use terminating thunks). I agree that within Lean it's Nat.

[Mario Carneiro]

You can't prove that nonstandard () is equal to succ nonstandard

[Kyle Miller]

I get that Mario

[Mario Carneiro]

you can prove it's succ of something but that something is a different object with a different address

[Mario Carneiro]

so you just made big - 1 and it's observably nonzero and provably not big

[Mario Carneiro]

even though it has exactly the same code as big itself

[Mirek Olšák]

Mario Carneiro said:

The question is how you define the lean axiomatic system Mirek Olšák . If you want to include native_decide "axioms" you need a model for how interpreter evaluation works and this is intensely machine-specific in a variety of ways

I would expect that there are still reasonable abstract computational models that could be used to define (part of) Lean's evaluation before we start looking into hardware limits but you know probably more than me here.

[Mario Carneiro]

Sure, it's an abstract hypercomputer which is nevertheless a 64-bit windows :)

[James E Hanson]

James E Hanson said:

Thanks but why then does

#eval (unsafeCast 4294967295 : Nat) = (4294967295 : Nat)

evaluate to true? Why isn't casting with an axiomatic equality the same as unsafe casting at runtime? (I checked and #eval (cast IntEqNat 4294967295 : Nat) = 4294967295 evaluates to false.)

Okay I knew I didn't hallucinate that there was something weird here. Why does this happen?

#eval (unsafeCast (4294967296 : Nat) : Int)
-- Evaluates to 4294967296.

#eval (unsafeCast (4294967296 : Nat) : Int) == (4294967296 : Int)
-- Evaluates to false.

#eval (unsafeCast (4294967296 : Nat) : Int) == (unsafeCast (4294967296 : Nat) : Int)
-- Evaluates to true.

#eval 4294967296 == (4294967296 : Int)
-- Evaluate to true.

[Mario Carneiro]

Most likely you are creating an ill-formed value, which behaves weirdly

[Mario Carneiro]

I recall there is some way to generate numbers that print as ***********

[James E Hanson]

Is this because Nat and Int have different upper bounds for when they switch runtime representations?

[Mario Carneiro]

that would make sense

[Mario Carneiro]

(they do)

[Mario Carneiro]

that number is apparently incomparable with zero

#eval (unsafeCast (4294967296 : Nat) : Int) > 0 -- false
#eval (unsafeCast (4294967296 : Nat) : Int) < 0 -- false
#eval (unsafeCast (4294967296 : Nat) : Int) == 0 -- false

[Mario Carneiro]

Mirek Olšák said:

Mario Carneiro said:

The question is how you define the lean axiomatic system Mirek Olšák . If you want to include native_decide "axioms" you need a model for how interpreter evaluation works and this is intensely machine-specific in a variety of ways

I would expect that there are still reasonable abstract computational models that could be used to define (part of) Lean's evaluation before we start looking into hardware limits but you know probably more than me here.

even without bringing up concrete limits, it is true that for any lean proof it can only do finitely many computations with native_reduce so there is a uniform bound on max recursion depth in all such computations

[Mirek Olšák]

Nothing against taking finite fragments of an infinite theory.

[Mirek Olšák]

@Kyle Miller If I understand correctly, you are saying that for a Lean programmer, a good mental model is something like Haskell / OCaml, with possibly infinite programs, and possibly infinite datastructures (coinductives). Unfortunatelly, this mental model is highly incompatible with Lean's logic, so logic-wise, big feels much more as a really large finite number than an infinite object.

[Aaron Liu]

having nonterminating programs implies the existence of nonterminating proofs

[Aaron Liu]

so I think it doesn't really conflict with the logic

[Mario Carneiro]

if there is a closed term of type False that's a problem whether or not the term normalizes

[Mirek Olšák]

Mario Carneiro said:

If it was possible to have recursion between a value and a function I think you could get an inconsistency, e.g.

mutual
partial def nonstandard : LazyNat := succ nonstandardF
partial def nonstandardF (_ : Unit) : LazyNat := nonstandard
end

What is the idea? I was a bit surprised that partial def cannot be a value but I don't see how I could exploit that (I was thinking if I could get inconsistency too).

[Kyle Miller]

@Mirek Olšák My assumptions: (1) we're talking about native_decide and looking at the consequences inside Lean, (2) so that means we care about a reasonable runtime model (not just a mental model) of data, and (3) the idea of 'nonstandard natural numbers' was brought up, which has a specific meaning, and the runtime type doesn't satisfy this (this third point is just to say "it seems worth being careful about what you mean by nonstandard").

Given these, I'm saying that the Lean compiler is effectively allowing you to use LazyNat as if it were the greatest fixpoint instead of the least fixpoint (hence coinductive instead of inductive). Let's agree the greatest fixpoint includes computationally diverging terms to be precise (so it's also not quite CoNat). And yes, the greatest and least fixpoint are highly incompatible with each other.

Since the Lean compiler assumes the programs you write are creating well-formed terms for the inductive type, what I was obliquely trying to get at earlier is that it might be possible to convince the compiler that some computation is impossible because it diverges, get it to eliminate it, then arrive at a contradiction through native_decide.

[Mario Carneiro]

Mirek Olšák said:

What is the idea? I was a bit surprised that partial def cannot be a value but I don't see how I could exploit that (I was thinking if I could get inconsistency too).

If nonstandard : LazyNat was a global constant, then it would have to be computed at initialization time and used as a closed value. As a result, all references to it will come out pointer-equal to one another, so if you start unfolding nonstandard you will get a sequence of succs all of which compare pointer-equal to nonstandard. This violates the model, which requires that they all be distinct nonstandard numbers.

[Mirek Olšák]

Is there a way to make use of pointer-equality in computation?

[Mario Carneiro]

I was a bit surprised to find that the closure object fun () => nonstandard () which appears inside the unfoldings of the original version are all distinct from one another, because the IR for these just say something like let x.0 := nonstandard which looks like it's loading a constant, but it seems to allocate a fresh closure every time

[Mario Carneiro]

yes, the native_decide model has to make pointer-equal values =

[Mirek Olšák]

Why?

[Mirek Olšák]

Is there an example where it skips evaluation because of pointer equality?

[Mario Carneiro]

docs#withPtrEq

[Mario Carneiro]

Here's an example of what goes wrong when pointer equality doesn't match =:

def foo : Bool := withPtrEq True False (fun () => false) fun eq => nomatch cast eq ⟨⟩
example : foo = false := rfl
#eval foo -- true
example : False := nomatch show foo = true by native_decide

[Mario Carneiro]

also: :double_exclamation:

[Kyle Miller]

Lol, who made it so Sort u : Type u :-)

[Mario Carneiro]

you can do the same proof with Nat = Bool, it's just more complicated. Any two types which are provably different can be used in that example

[Mirek Olšák]

I thought withPtrEq could be used to obtain equality from pointer equality. So far I see it used to a mysterious proof of False with evaluation. This is because the runtime doesn't see propositions / types?

[Kyle Miller]

(Goes to show once again type erasure is more complicated than you'd hope...)

You haven't reported this to the Lean 4 issue tracker, have you @Mario Carneiro? Happy to submit it if you haven't.

[Mario Carneiro]

no, I just noticed this flaw now

[Mario Carneiro]

@Mirek Olšák The type signature of withPtrEq is complicated, but the basic idea is that if two values of the same type are pointer-equal then you can obtain a proof that they are =

[Kyle Miller]

Gabriel seems to have noticed it in lean4#1502

[Mario Carneiro]

oh and @Rob23oba bumped that thread just yesterday :)

[Mario Carneiro]

@Mirek Olšák The types True and False are erased, so they both become the neutral value in the compiler and hence are pointer-equal, even though they are provably distinct

[Mario Carneiro]

@Kyle Miller I feel like the labels on lean#1502 don't really reflect the nature of the issue

[Kyle Miller]

Almost wish there was a NaN-like pointer that's not equal to itself, just to implement this efficiently.

(I can't convince myself this would be sufficient... Maybe it's sufficient for CSE to respect that these NaNs are not equal to each other, but that's likely a road leading toward inefficiently compiled code.)

[Mario Carneiro]

that was option 1 in gabriel's issue I think

[Mario Carneiro]

I think it would work, you just need a special erased value which means "the set of values this could represent are not necessarily all ="

[Mario Carneiro]

ideally this would be a marker on the ABI type rather than a value though

[Kyle Miller]

Some sort of "can do safe ptrEq" analysis seems appealing, since this should all be statically knowable, right? (Assuming monomorphizing is an acceptable cost.)

It seems like it's an a similar direction to an ST analysis we talked about at some point, that for soundness verification, it's sufficient to verify that the types can be faithfully represented using Lean's runtime types. (Or, for a less runtime-specific point of view, that it's possible to encode/decode the type's values using an "STValue" inductive; then we pretend ST actually is recording encoded STValue values.) This hasn't yet been a practical soundness issue though, right?

[Mario Carneiro]

I think withPtrEq is very difficult to use and so I haven't run into these issues much because I don't even try

[Mario Carneiro]

However, in lean4lean there is some use of ptrAddr which I manually monomorphized because I was worried about issues like this; that's not enough to make it sound though and it's not really practical to work inside a big quotient

[Mario Carneiro]

I'm not even sure it's possible for l4l in the sense that it can actually give different behaviors depending on caching order

[Mario Carneiro]

https://github.com/digama0/lean4lean/blob/master/Lean4Lean/PtrEq.lean

^ I'll be happy if you find a better way to do this

[Niels Voss]

Is this discussion somewhat related to the concept of omega-inconsistency? In particular the part about how you can prove big ≠ 0, big ≠ 1, big ≠ 2, and so on with native_decide if you had unlimited computational power.

[James E Hanson]

Yes, they're related.

[James E Hanson]

$\omega$-inconsistency is the same thing as not having an arithmetically standard model.

[Kyle Miller]

@James E Hanson Just to check, an arithmetically nonstandard model means it's still a model of peano arithmetic, right? The Lean runtime values for the LazyNat type don't form a model of peano arithmetic (one interpretation is that it's Nat with two extra elements: one for big and one for nonterminating computations).

[Kyle Miller]

I'm not even completely certain yet that you can't get the Lean compiler to 'prove' false (via native_decide) using big.

[Mario Carneiro]

@Kyle Miller The model being exposed here through native_decide evaluations has the following elements:

• Nat
• a doubly infinite sequence inf : Int -> Lazy such that inf n = succ (fun _ => inf (n-1))

There is no element for nonterminating computations. You can't observe (and hence obtain a native_decide axiom for) any computation that directly involves running a nonterminating subexpression.

[Mario Carneiro]

here inf 0 is nonstandard, inf (-n) are the sequence of values you obtain by pattern matching it and seeing the chain of succ's, and inf n are the values you can construct by wrapping it in succ's

[Mario Carneiro]

You can construct nonstandard' with the same definition and you will get another infinite sequence but you won't be able to relate any of the values to inf so it may actually be the same sequence

[Mario Carneiro]

when you "complete" this using lean logic to prove the existence of more elements given these, you end up with a nonstandard model of Nat.

[Mirek Olšák]

So the point is that if we define

partial def f (x : In) := ... f ... f ...

even through pointer equality, it is not possible to check that the inner f is the same as the outer f?

[Mario Carneiro]

basically yes, because f isn't itself a lean object, papp f #[env...] is, where env is some tuple of variables which are pre-applied to the function. In this case env is empty, but nevertheless papp f #[] doesn't have value semantics, it is generative so every time you run the code you get a new object. In some cases you might get lucky and it won't generate distinct objects but usually it will make a fresh object. It's not too different from the semantics of a constructor: (a, b) will construct a new tuple containing a and b, and every time you run code that does this you get an object with a different address, unless you get lucky and two objects are created near enough to be CSE'd together

[Mario Carneiro]

In your example, the "outer f" isn't a lean object but the inner one is. You have two uses of f, so they will most likely both refer to the same object, but if you call that object to recurse, the recursion will almost certainly generate a separate object for its two uses of f, even if x : In is just () : Unit

[James E Hanson]

Mario Carneiro said:

you end up with a nonstandard model of Nat.

What sense of the word 'model' are you using here specifically?

[Mario Carneiro]

what sense is there other than the usual?

[Mario Carneiro]

If we want a model of Nat that contains an infinite decreasing sequence of elements that's necessarily nonstandard

[James E Hanson]

I guess your phrasing makes it sound like you're somehow getting a specific non-standard model, rather than a theory whose models are all non-standard.

[Mario Carneiro]

I'm describing (envisioning) a model construction procedure, maybe something like a Henkin model

[Mario Carneiro]

where you start from some particular elements you've been told exist and then build all the things you can build from that

[Mario Carneiro]

The axioms you can extract here from native_decide are effectively the usual axioms for nonstandard PA: Nat is a type with an induction principle, also big is a nat and big > 0, 1, 2, ...

[Kyle Miller]

It seems to me that it would be good to be very clear about the assumptions here to say what "the" model being exposed is.

• First of all there's the runtime model itself. If we ignore pointer equality and only look at observable behavior, the elements are the standard natural numbers, plus nonstandard, plus nontermination. We can observe nontermination by proving properties of the runtime itself outside of Lean.
• Second, there's the runtime model itself with pointer equality. With this, the elements generated by nonstandard are the int n elements. It's possible to make programs that can distinguish between them.
• Third, there's this second runtime model, pulled back into Lean using native_decide, and then you take the logical consequence of these elements from within Lean. This takes a step from outside the theory though, where we use the observation that nonstandard doesn't equal any of the standard Nats to conclude it isn't any of them. It also takes the assumption that since LazyNat models the naturals, it must then be a nonstandard model. (However, only some of the nonstandard elements are obviously realized in the runtime model. The rest don't seem to be present, just posited. Maybe you can get the rest syntactically from within Lean using logic I don't know though.)

[Mario Carneiro]

The runtime model does not have a nontermination element

[Kyle Miller]

Says you Mario :slight_smile:. I can observe nontermination, and I can open up a debugger, see what's going on, and then prove it on paper.

[James E Hanson]

What is 'the runtime model'?

[Mario Carneiro]

@Kyle Miller Please prove it on paper

[Mario Carneiro]

I assert that there are no computations you can perform which give you an axiom out of native_decide saying a nontermination element exists

[Mario Carneiro]

that could be wrong but I want to see the counterexample if so

[Kyle Miller]

@James E Hanson It's the objects that the Lean runtime manipulates when evaluating something like nonstandard. It's not manipulating Lean expressions, but other sorts of objects.

[Kyle Miller]

@Mario Carneiro That's sort of my point — I didn't agree to the condition that observational behavior means I can import an axiom into Lean using native_decide. I think that's obscuring things. Hence my separating this into three different components. The third one doesn't admit nonterminating elements.

[Mario Carneiro]

• First of all there's the runtime model itself. If we ignore pointer equality and only look at observable behavior, the elements are the standard natural numbers, plus nonstandard, plus nontermination. We can observe nontermination by proving properties of the runtime itself outside of Lean.

What's missing here is that there is no bisimulation principle, so there can well be many elements which are all distinct and are all an infinite chain of succs

[Mario Carneiro]

just because two elements are observably equivalent doesn't mean they are the same in the runtime model or in the lean model

[James E Hanson]

Yeah, I was going to say, it should be fairly easy to build other terms like nonstandard that aren't provably or observably equal to nonstandard.

[Mario Carneiro]

the lean axioms are actually inconsistent with them being the same, and by mostly luck the runtime model also doesn't make them the same because of the allocation semantics

[James E Hanson]

This is probably a minor point, but the runtime model isn't really a 'model' in the sense we were discussing a moment ago, right?

[Mario Carneiro]

It is a partial model?

[Mario Carneiro]

It is kind of a "ground truth" we can use to obtain lots of axioms by evaluation

[Mario Carneiro]

native_decide effectively says anything observably true in the runtime model is admitted as an axiom

[James E Hanson]

So you're conceptualizing it as a model in the sense that we can query it in order to determine facts without actually proving them, right?

[Mario Carneiro]

yes basically

[Mario Carneiro]

I think it walks and talks like a model though

[Mario Carneiro]

maybe universal sentences are dicey on it

[Mario Carneiro]

it is a model in the sense that it has a domain of objects and an interpretation of functions

[Mario Carneiro]

the objects are all of the things you could construct via computation of lean expressions

[Mario Carneiro]

but I'm not sure it has a well formed notion of equality on it or a general interpretation of the = function

[James E Hanson]

Sure, I understand the fact that the word 'model' is often used in a more general sense.

I just think it's maybe a little bit important to highlight the fact that this is something akin to the notion of a(n intuitionistic) term model in type theory. It isn't going to be a model of Lean with classical choice (and therefore LEM).

[Mario Carneiro]

unclear?

[James E Hanson]

Well you certainly don't have an implementation of, say, a halting oracle in the Lean runtime model.

[Mario Carneiro]

There are lots of things that diverge, so sometimes instead of "yes or no" you get "yes or diverge"

[Mario Carneiro]

so the interpretation of functions is partial

[Kyle Miller]

@Mario Carneiro, if you want to stick to native_decide being the arbiter here, then tell me why I should be convinced that nonstandard isn't one of the standard natural numbers?

[James E Hanson]

I thought that Mario had said that given the recursion limit in practice, you could think of nonstandard as being a large standard natural number?

[James E Hanson]

@Mario Carneiro Does the runtime model make explicit decisions about equality of types? Or is that related to your earlier comment about =?

[Kyle Miller]

Even without that recursion limit, it seems inconsistent to me to say that nonstandard is nonstandard, if the only admissible interpretation of terms is via native_decide.

[Mario Carneiro]

As I mentioned above, you very well can. The issue is that if you decide nonstandard is 37 then later you might have a computation that invalidates this interpretation. If you want a single interpretation that is stable under future axioms you could get from a hypothetical future native_decide evaluation, and the computer on which is runs is abstracted and has no implementation limits, then you get the axiom system big > 0, 1, ... which is nonstandard PA

[Mario Carneiro]

@James E Hanson No it does not, there are no type equalities you can resolve one way or another using native_decide

[Kyle Miller]

You're doing reasoning outside of Lean there though, right? Why can you do that, but I can't say "native_decide diverges here"

[Mario Carneiro]

I'm meta-reasoning about the axiom system specified by a hypothetical lean typechecker with unbounded memory

[Mario Carneiro]

If native_decide diverges, then you don't get an axiom

[Mario Carneiro]

the definition of the native_decide axiom schema is that you run the program, observe it returns true, then accept the boolean is equal to true as an axiom

[Mario Carneiro]

so if you define partial def loop : Bool := loop then you get no native_decide axiom proving it is equal to either true or false because if you try to work with it the computation diverges so you get nothing

[Mario Carneiro]

by contrast, the nonstandard : LazyNat because of laziness can be unfolded and so you can observe it has at least n succs for each n

[James E Hanson]

By the way, when I was playing around with native_decide, I never saw an instance of it using Lean.ofReduceNat. When does this happen?

[Mario Carneiro]

and so the theoretical extent of all axioms you can extract from this object is the set of all such big > n axioms

[Mario Carneiro]

unless you can find another way to use native_decide to find more things about the object

[Mario Carneiro]

ofReduceNat is never used by lean, I think it can be deleted

[Mario Carneiro]

you can use it manually or in a tactic if you want but there isn't much need for it

[James E Hanson]

What is the point of having both Lean.trustCompiler and Lean.ofReduceBool?

[Mario Carneiro]

this is a workaround for the fact that you can prove extra things already just using reduceBool without ofReduceBool

[James E Hanson]

Ah, what's an example of that?

[Mario Carneiro]

if you put a nondeterministic function in there you can prove false

[James E Hanson]

Is it possible for something to only use Lean.ofReduceBool? I'm guessing not because even this doesn't work:

theorem ofReduceBoolTest : Lean.ofReduceBool = Lean.ofReduceBool := rfl

#print axioms ofReduceBoolTest
-- 'ofReduceBoolTest' depends on axioms: [Lean.ofReduceBool, Lean.trustCompiler]

[Mario Carneiro]

#lean4 > soundness bug: native_decide leakage @ 💬

[Mario Carneiro]

As long as you define axiom tracking such that it looks at the types of axioms, no it's not possible because ofReduceBool has a type which uses reduceBool which uses trustCompiler

[James E Hanson]

Mario Carneiro said:

#lean4 > soundness bug: native_decide leakage @ 💬

I assume this isn't still possible because the way IO works changed?

[Mario Carneiro]

it doesn't matter, you can use extern for the same effect

[Mario Carneiro]

it's just defined as not a problem now

[James E Hanson]

Mario Carneiro said:

it doesn't matter, you can use export for the same effect

As in using implemented_by?

[Mario Carneiro]

I guess you could use that as well, with some unsafePerformIO or whatever it's called

[Mario Carneiro]

extern lets you write C code which obviously can be impure

[James E Hanson]

What is 'export' in this context then?

[Mario Carneiro]

sorry, I meant extern

[Mario Carneiro]

@[extern my_c_function] opaque myLeanFunction : Nat -> Nat

[Mario Carneiro]

lean_object* my_c_function(lean_object* x) { return ... }

[Mario Carneiro]

something like that

[Paul Reichert]

Mirek Olšák said:

Well, once we have a nonstandard natural number big : Nat, then this should be at least an eval-consistent interpretation of partial def , right?

You might be interested in the approach that popped up in my head after reading your ideas: #lean4 > Extrinsic termination proofs for well-founded recursion @ 💬 In short, the idea is to use a partial function returning a subtype. If chosen wisely, the subtypes contain enough information for proving fixpoint equations for it after the fact, even in def f x := ... f (f (x/2)) ... situations. We get a computable fixpoint (that might run forever) and don't need to use any unsafe language features.

It looks like this:

def Pred (F : ((a : α) → β a) → ((a : α) → β a)) (a : α) (b : β a) : Prop := sorry /- omitted -/

partial def fixAttach [Nonempty ((a : α) → β a)] (F : ((a : α) → β a) → ((a : α) → β a)) (a : α) :
    Subtype (Pred F a) :=
  ⟨F (fixAttach F · |>.val) a, by sorry /- omitted here -/⟩

def fix [Nonempty ((a : α) → β a)] (F : ((a : α) → β a) → ((a : α) → β a)) (a : α) : β a :=
  (fixAttach F a).val

def f91.functional (recurse : Nat → Nat) (n : Nat) : Nat :=
  if n > 100
    then n - 10
    else recurse (recurse (n + 11))

def f91 (n : Nat) : Nat :=
  fix f91.functional n