expr.replace

Stream: general

[Jakob von Raumer]

Is there a version of expr.replace that performs replacements until a fixed point is reached?

[Mario Carneiro]

I think you need something like ext_simplify_core for that kind of fine-grained traversal control

[Mario Carneiro]

If you don't mind that it doesn't actually stop traversal, you can use option or other monadic stuff to escape once you find what you wanted

[Mario Carneiro]

Or you could write your own, expr.replace is a simple recursive function IFIACT

[Jakob von Raumer]

ext_simplify_core is not useful if I really want to modify the expression, right?

[Jakob von Raumer]

Maybe the easiest would just be to calculate how many times I'd have to run expr.replace...

[Jakob von Raumer]

To be more explicit: I want to replace all occurences of (f a b c ...) where f is a local_const by something else, but I struggle with the fact that the expr.app with the f is the innermost one and not the outermost one...

[Sebastian Ullrich]

Why do you need the number of runs? You're in meta land, so you don't have to worry about proving termination, do you?

[Jakob von Raumer]

True that...

[Jakob von Raumer]

Still have to get used to being that dirty

[Sebastian Ullrich]

:)

[Jakob von Raumer]

But I cannot imagine that there's not a suitable version of expr.is_app_of somewhere, such that (expr.app (expr.app (expr.const `lt []) (expr.var 1)) (expr.var 0)).is_app_of `lt'actually evaluates to tt...

[Simon Hudon]

@Sebastian Ullrich You should be ashamed to corrupt the youth (or user base) like this! Proposing to not think about termination ... Where is the world heading to?

[Sebastian Ullrich]

We'll soon enough introduce a fuel type to make the new parser actually implementable in total Lean... :)

[Simon Hudon]

Awesome! How does fuel work?

[Mario Carneiro]

Why isn't it currently implementable?

[Sebastian Ullrich]

It's basically nat, but provides an opaque constant that is assumed to be large enough that the code generator can just ignore the type in practice... :)

[Sebastian Ullrich]

So it's just a hint to the code generator

[Mario Carneiro]

Wouldn't it be better to just do a well founded recursion with an omitted proof?

[Jakob von Raumer]

But I cannot imagine that there's not a suitable version of expr.is_app_of somewhere, such that (expr.app (expr.app (expr.const `lt []) (expr.var 1)) (expr.var 0)).is_app_of `lt'actually evaluates to tt...

God damn it, there's a ' in the end of that line...

[Moses Schönfinkel]

But you can prove so easily that fuel is nicely structurally decreasing! :P

[Mario Carneiro]

The point is it's a lie though

[Mario Carneiro]

the real fuel is infinity, which is not well founded, I think we should be honest about that

[Moses Schönfinkel]

I admit nothing, deny everything. It proofchecks, surely it must be correct ;).

[Moses Schönfinkel]

(It's a minor detail that it doesn't model whatever it is I had set out to do.)

[Mario Carneiro]

Alternatively, the VM could support some coinductive type

[Sebastian Ullrich]

@Mario Carneiro What does omitted mean, sorry? Things like macro expansion will be _provably_ non-wellfounded, as long as we don't restrict the user input.

[Mario Carneiro]

undefined actually, but yes

[Mario Carneiro]

I would rather have a sign that says "this is false, but that won't stop me" than a shell game that is false but not obviously so

[Sebastian Ullrich]

We want non-meta definitions to prove partial correctness of them. There is no need for fuel in meta.

[Mario Carneiro]

Why not use coinductive types? That's what they are for

[Mario Carneiro]

I don't mean supporting some coinductive command mind you, just some specific useful/relevant coinductive type, like mathlib computation

[Mario Carneiro]

which is basically "programming with fuel"

[Mario Carneiro]

The problem is that models of coinductive types in CIC are not computationally efficient (i.e. stream as a nat -> A instead of B -> A x B), so they need to be VM reimplemented

[Sebastian Ullrich]

Yeah, I'm not looking forward to that.

[Sebastian Ullrich]

I agree that computation may be a more satisfying design (it shouldn't matter for the proofs), but any trampolining will be bad for performance

[Mario Carneiro]

Trampolining how? B -> A x B is exactly the same as the state monad, and it didn't seem to be a big problem there; I assumed the plan was to optimize the trampoline away once lean compilation gets good

[Mario Carneiro]

Speaking of which, this requires a trivial amount of VM support - "call Y instead of X", and it would solve a huge number of problems if an API for that was exposed

[Mario Carneiro]

Other applications include "VM identity functions", where some nontrivial lean function is the identity in VM representation, while executing it as written will have much worse performance (for example, list.attach is O(n) but is a VM identity function)

[Sebastian Ullrich]

It sounds like we would have to specialize the trampoline driver to the specific functional, but I don't expect specialization any time soon

[Sebastian Ullrich]

"call Y instead of X" sounds like trouble if the types of Y and X have different runtime representations like in your first example...?

[Simon Hudon]

I like Mario's thinking. Using computation instead of the fuel trick has the added benefit that, if you call one of those functions in code where precise knowledge about termination matters, the type tells you exactly what to expect. And a computation + proof of termination gives you a properly well-founded Lean value

[Simon Hudon]

An example where I have seen that separation to be productive is when the proof of termination depends on the shape of a pointer structure

[Simon Hudon]

If that's useful, I have a Lean port of Chlipala general recursion machinery.

[Sebastian Ullrich]

Chlipala appears to list some strong limitations for both of his coinductive definitions

[Mario Carneiro]

"call Y instead of X" sounds like trouble if the types of Y and X have different runtime representations like in your first example...?

It's okay as long as it's a complete type replacement, i.e., all the functions that access the type are replaced with modified versions. For example, we could VM-replace nat.add withnum.add, and also all the other nat functions, if we wanted to have a lean-based fast nat implementation. Similarly, you could use this to support the quotient encoding: you don't VM-replace quot A by A because it's a type so it won't be called anyway, but you replace all the quot functions with identity functions.

If we ever get the ability to write system F functions for direct use by the VM (although this is a whole separate feature), it would also be useful to use VM replacement here, in case a certain function can't be well-typed in lean but is valid system F.

[Mario Carneiro]

It sounds like we would have to specialize the trampoline driver to the specific functional, but I don't expect specialization any time soon

Thinking more about how this would actually work with computation, we have computation.run which calls the corecursor (which has type B -> A + B after VM-replacement), returns A if success, and otherwise calls itself with the new value of B. This function is the "trampoline" in your scenario. On the other side, the coinductive type is being represented by the corecursor itself, so the user wrote this function B -> A + B. You would have to call the B part whenever you need to use some fuel, and otherwise return the output or continue some other well-founded recursion etc.

Part of the problem with programming this way is that B must contain the entire state of the program, everything that changes during the recursion, and it's usually unpleasant to have to explicitly enumerate all this data - this is what the compiler should be doing for you. One really nice way to handle this would be to have a compiler from unbounded recursive definitions to computation, or even simpler, a computation.fix operator which allows you to write such functions directly. (Apparently there is no computation.fix defined, but it isn't hard to define, with type (A -> computation A) -> computation A.)

[Mario Carneiro]

With this latter approach, you could just call fix f instead of computation.run (computation.fix (ret o f)) on the VM side and thus avoid most of the trampolining. There would still be fix(f) { return f(fix(f)); } which I guess can be inlined(?) but otherwise seems difficult to improve on

[Sebastian Ullrich]

It's okay as long as it's a complete type replacement

I see, yes. We're planning to allow private fields in structures to hide implementation details like string, which could be used here as well

[Sebastian Ullrich]

One really nice way to handle this would be to have a compiler from unbounded recursive definitions to computation

This would be a nice feature for a future equation compiler defined in Lean. With fix, you still have to pack multiple arguments into tuples. Though that could also happen automatically when lifting computation through state_t.

[Simon Hudon]

I can see a lot of use for a new generation of equation compilers (including some for corecursive functions). For computation specifically, it would be nice if it worked on the basis of a type class. If your return type is a monad that supports unbounded recursion, then its amenable to the treatment of the new equation compiler.

[Sebastian Ullrich]

I will be very happy if all of this works out some day :)

[Sebastian Ullrich]

Still not sure I should use it in the parser :smile:

[Mario Carneiro]

Why not put a limitation on how many nested macros to unfold? Seems like that would be undesirable anyway

[Sebastian Ullrich]

Yes, that's what it currently looks like. There may be better examples, like parsing routines where we don't want to prove wellfoundedness without the tactic framework.

[Simon Hudon]

That is also a problem with unbounded recursion: you need to prove that your functions are monotonic. The tactic framework is useful for that. Maybe we can do it with type classes too though

[Mario Carneiro]

This is part of the reason I want to avoid the fuel approach - the functions of interest are not all functions, but functions that have some monotonicity conditions as fuel changes, and you have to prove this for all functions you define, even though the proof is always straightforward.

[Simon Hudon]

But I have found the (H : monotonic f . prove_monotonicity) notation to be pretty useful to make that invisible

[Simon Hudon]

(in the parameters of fix for instance

[Mario Carneiro]

Not sure how much of this is available in the parser stuff though (maybe bootstrapping will help here)

[Chris Hughes]

What does expr.replace do?

[Keeley Hoek]

So because of expr.app and other such things an expr is a big tree of little-er exprs. You can get lean to map over an expr in this way with a function which can decide to replace subexpressions or not (the function decides to either a) replace this with something I provide or b) don't replace and descend into it instead). The nat argument tells you how deep in the binders you are, so you can correctly emit expr.vars.

[Chris Hughes]

Thanks. Sounds like what I wanted.

[Edward Ayers]

added docstring to https://github.com/EdAyers/lean

[Chris Hughes]

Struggling to use expr.replace slightly. I want to use infer_type to fill in the (expr → ℕ → option expr) argument, but this returns a tactic expr not an expr or option expr. Is there any way around this?

[Kenny Lau]

so just extract the expr?

[Kenny Lau]

t <- infer_type u

[Mario Carneiro]

no way around it, I'm afraid. infer_type wouldn't even work because it's looking at open terms

[Mario Carneiro]

you have to explicitly traverse the term and instantiate_local to go through binders

[Mario Carneiro]

tactic.hide is an example

[Chris Hughes]

Okay thanks.