Stream: general

Topic: understanding why functional extensionality blocks computati

Peter Hoffmann (Mar 06 2019 at 09:00):

I can't get my head around what is going on with the example of function extensionality blocking computation at https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

Does someone have some clarifying words, or know where I could search for some?

Moses Schönfinkel (Mar 06 2019 at 09:05):

Suppose f is long matrix multiplication and suppose g is strassen. Surely, for all matrices m m', f(m, m') = g(m, m'). Then the axiom of extensionality says that f must be equal to g, which is intensionaly untrue, because I'm using two different multiplication functions.

Moses Schönfinkel (Mar 06 2019 at 09:09):

A slightly better example is something unary so that the axiom needs to be invoked once only. Therefore, suppose we have quick sort and bubble sort. Then for any sequence with linear order s, quick_sort(s) = bubble_sort(s), aka. equivalent outputs for equivalent inputs, as they both sort the sequence. But the axiom of functional extensionality then says that quick_sort = bubble_sort, which loses their computational context.

Peter Hoffmann (Mar 06 2019 at 09:16):

I understand the basic idea.. (maybe), but how could I see the problem in a more concrete example of Lean code, and see how trying to reduce an expression leads to a problem? Is there maybe a way to see the kernel try to reduce a problematic expression and get into an infinite loop or something?

Peter Hoffmann (Mar 06 2019 at 09:18):

Unfortunately the words intensionaly untrue and computational context, don't mean much to me :(

Moses Schönfinkel (Mar 06 2019 at 09:24):

I've just taken a look at the chapter, it actually contains the sort of example you're looking for, in 11.3.

Peter Hoffmann (Mar 06 2019 at 09:27):

The problem is I don't understand what is happening with the example. How would the rules of Lean try to reduce the expression? Where is the problem?

Peter Hoffmann (Mar 06 2019 at 09:30):

Is the problem that you can't even apply the reduction rules to this expression, or is the problem that if you do, you will be reducing forever?

Peter Hoffmann (Mar 06 2019 at 09:35):

I mean somehow, I get that x is turned into 0 + x, and that is turned into 0 + 0 + x and so on..

Andrew Ashworth (Mar 06 2019 at 09:39):

If you really want to dig deep

Andrew Ashworth (Mar 06 2019 at 09:40):

All the rules Lean uses to reduce terms are described in detail

Andrew Ashworth (Mar 06 2019 at 09:42):

specifically, you'll want to read up on iota reduction

Andrew Ashworth (Mar 06 2019 at 09:42):

(and if you're not familiar with them, all the other greek letter reductions too)

Scott Morrison (Mar 06 2019 at 09:45):

There must be some level of intermediate explanation, before we get down to the actual reduction rules written in gobbledygook (sorry, Mario :-)

Peter Hoffmann (Mar 06 2019 at 09:48):

Intermediate explanation would be nice.

Chris Hughes (Mar 06 2019 at 10:05):

More or less, it's because the iota reduction rules mean recursors reduce when applied to a constructor. In this case the recursor is eq.rec and the constructor is eq.refl. But the equality proof wasn't constructed with eq.refl, and moreover cannot be constructed with eq.refl, so it cannot reduce.

Chris Hughes (Mar 06 2019 at 10:08):

If it did reduce, the resulting expression might not even type check.

Moses Schönfinkel (Mar 06 2019 at 10:14):

But this only speak to consequences of the way the reduction is defined in Lean. I think Peter's asking why they're set up in such a way (to which I can only provides an answer that goes full circle, because it avoids issues with functional extensionality).

Andrew Ashworth (Mar 06 2019 at 10:18):

I don't quite follow

Andrew Ashworth (Mar 06 2019 at 10:18):

Why is it set up this way? It's because extensionality breaks strong normalization of terms

Andrew Ashworth (Mar 06 2019 at 10:19):

You can make goofy terms that will cause the type checking to never terminate, if I remember correctly

Moses Schönfinkel (Mar 06 2019 at 10:20):

An example of one such term is what I thought Peter was looking for :).

Peter Hoffmann (Mar 06 2019 at 10:20):

I mean, it would be nice to have a precise definition of "computational content", and a proof that functional extensionality breaks this.

Peter Hoffmann (Mar 06 2019 at 10:21):

I mean, "computational content" is a very abstract thing. Goes beyond how lean works.

Peter Hoffmann (Mar 06 2019 at 10:23):

But this is getting to a bit meta level, with what language is one supposed to prove such a thing.

Andrew Ashworth (Mar 06 2019 at 10:24):

computational content: anything that isn't a proposition

Andrew Ashworth (Mar 06 2019 at 10:25):

proof that functional extensionality breaks this: exactly 11.3 in theorem proving in lean :(

Andrew Ashworth (Mar 06 2019 at 10:26):

just take it on faith

Andrew Ashworth (Mar 06 2019 at 10:27):

unless you want to spend time learning the lambda calculus reduction rules and working out some examples

Chris Hughes (Mar 06 2019 at 10:27):

Here's an example from a thread a while ago

lemma not_refl : true = (true ∨ false) :=
propext (by simp)

def does_not_reduce_to_zero : ℕ :=
@eq.rec_on _ _ (λ _, ℕ) _ not_refl \$
0

#print axioms does_not_reduce_to_zero
set_option pp.proofs true
#reduce does_not_reduce_to_zero
#eval does_not_reduce_to_zero


Chris Hughes (Mar 06 2019 at 10:31):

Here's a better example

import data.multiset

open nat

def S : multiset ℕ := quot.mk _ [1,2]

def T : multiset ℕ := quot.mk _ [2,1]

lemma S_eq_T : S = T := dec_trivial

def X (m : multiset ℕ) : Type := {n : ℕ // n ∈ m}

def n : X S := ⟨1, dec_trivial⟩

def n' : X T := eq.rec_on S_eq_T n

#reduce n'


Chris Hughes (Mar 06 2019 at 10:33):

If the eq.rec in the definition of n' cannot reduce, because n has type X S, which is not definitionally equal to X T, so it would no longer type check after reduction.

Last updated: May 16 2021 at 21:11 UTC