[Agda] Erasable vs. irrelevant

[Andreas Abel]

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/