understanding why functional extensionality blocks computati

Stream: general

[Peter Hoffmann]

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]

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]

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]

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]

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

[Moses Schönfinkel]

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]

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]

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]

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]

If you really want to dig deep

[Andrew Ashworth]

read: https://github.com/digama0/lean-type-theory/releases

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Scott Morrison]

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

[Peter Hoffmann]

Intermediate explanation would be nice.

[Chris Hughes]

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]

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

[Moses Schönfinkel]

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]

I don't quite follow

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Moses Schönfinkel]

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

[Peter Hoffmann]

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

[Peter Hoffmann]

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

[Peter Hoffmann]

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

[Andrew Ashworth]

computational content: anything that isn't a proposition

[Andrew Ashworth]

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

[Andrew Ashworth]

just take it on faith

[Andrew Ashworth]

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

[Chris Hughes]

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]

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]

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.