michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Disable eta-reduction for now.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-01 23:19:34 -07:00
parent c13b9a792a
commit a8c77ff40e
1 changed files with 14 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/kernel/normalize.cpp
View file

@ -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) {