From a8c77ff40e0d4d9f785b0b5a74125a9175ab324d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Aug 2013 23:19:34 -0700 Subject: [PATCH] Disable eta-reduction for now. Signed-off-by: Leonardo de Moura --- src/kernel/normalize.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/kernel/normalize.cpp b/src/kernel/normalize.cpp index 56d8a60cb..fc8badfa7 100644 --- a/src/kernel/normalize.cpp +++ b/src/kernel/normalize.cpp @@ -76,6 +76,19 @@ class normalize_fn { lean_assert(is_lambda(a)); expr new_t = reify(normalize(abst_type(a), c, k), k); expr new_b = reify(normalize(abst_body(a), extend(c, value(k)), k+1), k+1); + return lambda(abst_name(a), new_t, new_b); +#if 0 + // Eta-reduction + Cumulativity + Set theoretic interpretation is unsound. + // Example: + // f : (Type 2) -> (Type 2) + // (lambda (x : (Type 1)) (f x)) : (Type 1) -> (Type 2) + // The domains of these two terms are different. So, they must have different denotations. + // However, by eta-reduction, we have: + // (lambda (x : (Type 1)) (f x)) == f + // For now, we will disable it. + // REMARK: we can workaround this problem by applying only when the domain of f is equal + // to the domain of the lambda abstraction. + // if (is_app(new_b)) { // (lambda (x:T) (app f ... (var 0))) // check eta-rule applicability @@ -93,6 +106,7 @@ class normalize_fn { } else { return lambda(abst_name(a), new_t, new_b); } +#endif } expr reify(value const & v, unsigned k) {