[Agda] Erasable vs. irrelevant
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Jan 17 09:31:18 CET 2012
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/
More information about the Agda
mailing list