[Agda] Erasable vs. irrelevant

[jleivent at comcast.net]

Thanks for the explanation, Andreas.  I wasn't thinking of termination witnesses - but that certainly is an obvious case of something erasable that is far from being irrelevant (at least in the informal sense).  Are there other cases not involving termination?

I have this intuition of erasable as meaning that the runtime cannot extract any information from something.  Which seems to imply that, for something to be erasable, it must lack discrimination.  For example, take the following axiomatic definition of Naturals:

1. N : Set
2. zero : N
3. suc : N -> N
4. suc-injectivity: forall (n1 n2 : N) -> (suc n1 == suc n2) -> (n1 == n2)
5. zero-suc-discrimination: forall (n : N) -> (suc n == zero) -> bottom

I think this definition of N is not erasable precisely when the discrimination axiom (5) is used - because it enables decisions to be made based on differences between Ns.

But if one either removes the discrimination axiom, or instead weakens it to the following axiom:

5'. weak-zero-suc-discrimination: forall (n : N) -> (suc n == zero) -> (forall (n1 n2 : N) -> (n1 == n2))

then the resulting type seems entirely erasable, just because, given any two N's, there is no proof that they are different.  But, is it really erasable?  Or, am I missing something?  The above N - without discrimination or with the weakened version - is compatible with actual naturals (compatible in the sense that the actual naturals can supply proofs for the above "axioms" - so that if a module is parameterized by those axioms, then it can be instantiated with actual N) - and is also compatible with N = top - which is the quintessential erasable type. 

My understanding of irrelevant is that the instances of an irrelevant type are treated as equal - which certainly implies there is no proof that any two are different (no discrimination), but goes further.  The above Ns either without discrimination or with the weakened version of discrimination are not irrelevant in that sense.

It seems like a large part of a type's usefulness remains intact if you remove discrimination (or weaken it) - much more than if you just made all of the instances equal (although dealing with certain proof terms is easier if all instances of each proof type are assumed equal - standard proof irrelevance).  I found the above weakened discrimination very useful for erasing the "black level" terms in a newer version of that red black tree code I sent in last week.  But if this notion of erasability is mistaken, then what I did in that code was wrong.

I also didn't understand two other parts of your response.  One was the statement that "Eraseability concerns program extraction *after* type checking is 
complete."  Certainly - but irrelevant terms are still type checked, right?  They would be completely useless if they weren't.

The other was: "However, what if there is an assumed proof of  forall a a' -> a = a  in your context?  Then you can prove that f is irrelevant even if it is not."  What did you mean by "prove that f is irrelevant even if it is not"?  I'm assuming you meant "f is irrelevant in its first argument" - it's the "even if it is not" part that I don't understand.  If there is a proof that all a's are equal, then certainly all uses of a's are irrelevant, aren't they?


----- Original Message -----
From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: jleivent at comcast.net
Cc: agda at lists.chalmers.se
Sent: Tue, 17 Jan 2012 08:31:18 -0000 (UTC)
Subject: Re: [Agda] Erasable vs. irrelevant

Hello Jonathan,

On 17.01.12 2:42 AM, jleivent at comcast.net wrote:
> I'm quite confused about these two concepts - as to whether they are
> the same or not.

They are not the same.  More stuff is erasable than irrelevant.  This is 
because irrelevance maintains termination of *open* terms, i.e., terms 
with free variables that can have empty types.

Eraseability concerns program extraction *after* type checking is 
complete.  For instance, termination witnesses can be erased, but are 
not irrelevant (otherwise, they would not witness termination).

> Are all erasable terms irrelevant?
No.

> The confusing aspect to me is the
> requirement that irrelevant instances of the same type are treated as
> if they are all equal.  What if, instead of the instances being all
> equal, there just is no way to prove that two aren't equal?  Isn't
> that good enough to make them erasable (because no runtime decisions
> can be based on any differences in them)?  Are they then also
> irrelevant?  Or is this something that is erasable but not
> irrelevant?

When you say "there is no way to prove that two aren't equal" are you 
appealing to classical logic?  (Probably not.)

I guess you want a more extensional concept of irrelevance, in the 
following sense.  If you can *prove* that

   f a = f a'  for all a,a' in A

then f is irrelevant in its first argument.  However, what if there is 
an assumed proof of  forall a a' -> a = a  in your context?  Then you 
can prove that f is irrelevant even if it is not.

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/