[Agda] Erasable vs. irrelevant

[Andreas Abel]

Hello Jonathan,

On 1/17/12 7:32 PM, jleivent at comcast.net wrote:
> 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?

There is also inhabitants of the equality type.  They are not 
irrelevant, refl must be distinguished from neutral terms such as 
variables, in order to block reduction of subst for only assumed (but 
not necessarily true) equations.

> 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.

As I see it, your Naturals are erasable in both axiomatizations.  Axioms 
5 and 5' do not allow you to *computably* distinguish between zero and 
suc, only *logically*.  You cannot recover from absurdity.  Absurdity, 
hence Axiom 5, only allows you do eliminate impossible cases in a case 
distinction, but not to perform the case distinction itself.

Unless you add an induction axiom (scheme) or at least case distinction, 
there is no means of definition any function, like addition etc., hence, 
no computational content in N.

> 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.

Mmh, in my view, the empty type is also free of computational content, 
it should only be inhabited in unreachable branches of your program, 
which, ideally, are gone from the compiled code.

> 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.

Yes, they are type-checked.  However, they are irrelevant for 
computation at compile-time (which occurs also inside function bodies, 
hence non-empty contexts, when checking equality).  Eraseable terms are 
involved in compile-time computation.

> 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?

This is a distinction of "built-in" vs. "provable".  In built-in 
equality, true is different from false (as members of type Bool). 
However, you can easily prove that true equals false, under suitable 
assumptions.  Thus, even if you can prove that f true = f false (under 
some assumptions), you cannot let f be irrelevant in its first argument 
in the "built-in" type theory.

It all boils down whether you have assumptions or not.  Compile-time 
computation is done under assumption, thus, the concept of equality 
needs to be weaker than for the run-time scenario.  There, only closed 
terms are computed, there are no assumptions, and the suitable equality 
concept is the strongest one, observable equivalence.

Cheers,
Andreas

> ----- 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/