Zulip Chat Archive

Stream: general

Topic: understanding why functional extensionality blocks computati


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Peter Hoffmann (Mar 06 2019 at 09:18):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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..

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 09:39):

If you really want to dig deep

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 09:39):

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

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 09:40):

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

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 09:42):

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

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 09:42):

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

view this post on Zulip 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 :-)

view this post on Zulip Peter Hoffmann (Mar 06 2019 at 09:48):

Intermediate explanation would be nice.

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Mar 06 2019 at 10:08):

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

view this post on Zulip 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).

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 10:18):

I don't quite follow

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 10:18):

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

view this post on Zulip 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

view this post on Zulip Moses Schönfinkel (Mar 06 2019 at 10:20):

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

view this post on Zulip 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.

view this post on Zulip Peter Hoffmann (Mar 06 2019 at 10:21):

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

view this post on Zulip 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.

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 10:24):

computational content: anything that isn't a proposition

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 10:25):

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

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 10:26):

just take it on faith

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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'

view this post on Zulip 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