[Agda] Pattern matching on irrelevant data
Andreas Abel
andreas.abel at ifi.lmu.de
Mon Oct 3 23:42:45 CEST 2011
Thanks, Doel, that gives me a load to think about.
As you observed correctly, reduction of irrelevant matches had not been
implemented, I fixed this with my latest patch (just now).
Currently, strong normalization is not lost, because subst still only
reduces if the equivalence proof is refl. But you got a point here,
this is not very principled, since refl is as good as any other equality
proof in irrelevant position.
I think irrelevant matching against refl should be forbidden, (however,
this means some extra work for me), because it creates the additional
information that x is equal to y. Irrelevant matching is only sound if
it does not give extra type information.
@Conor: As far as termination checking is concerned, the termination
checker is based on structural ordering and this one cannot lie. A meta
variable or postulate is never structurally smaller than anything. The
termination checker does not honor equality of irrelevant things. If it
did, it would surely be fooled by lies.
But again, if e.g. in case of well-founded recursion the match on the
acc-constructor does not take place, then strong normalization is lost.
Stuff to think about.
Cheers,
Andreas
On 03.10.11 10:51 PM, Dan Doel wrote:
> This change appears to have irrelevant equality elimination as a
> special case. One has to be careful about this, because something like
> the following can occur:
>
> -- snip --
>
> module EqIrr where
>
> open import Relation.Binary
> open import Relation.Binary.PropositionalEquality hiding (subst)
> open import Relation.Unary
> open import Relation.Nullary
>
> open import Data.Empty
>
> subst : ∀{i j} {A : Set i} (P : A → Set j) {x y : A} → .(x ≡ y) → P x → P y
> subst P refl Px = Px
>
> roll : .((¬ ⊥) ≡ ⊥) → (⊥ → ⊥) → ⊥
> roll eq = subst (λ T → T) eq
>
> rick : .((¬ ⊥) ≡ ⊥) → ⊥ → ⊥ → ⊥
> rick eq = subst (λ T → T) (sym eq)
>
> rick-roll : .((¬ ⊥) ≡ ⊥) → ⊥
> rick-roll eq = ω (roll eq ω)
> where
> ω : ⊥ → ⊥
> ω b = rick eq b b
>
> -- rick-roll = λ. eq → ω (roll eq ω)
> -- ⟨erase⟩
> -- = ω (roll ω)
> -- = rick (roll ω) (roll ω)
> -- = rick (subst ω) (roll ω)
> -- = subst (subst ω) (roll ω)
> -- = subst ω (roll ω)
> -- = ω (roll ω)
>
> -- snip --
>
> Since the equality argument is allegedly irrelevant to subst, it can
> be erased, and subst just always computes. Currently this doesn't
> happen, but it appears to be due to that version of subst simply
> _never_ computing, even if refl is supplied directly (subst P refl Px
> simply reduces to subst P _ Px).
>
> This isn't a soundness issue, but it's a strong normalization issue,
> as normalization may need to happen in inconsistent contexts, and
> terms can loop if we don't get stuck on the neutral, false terms.
>
> I'd also add: the irrelevance in Agda seems to be mixing two different
> things. The reducing of irrelevant arguments to _ during type checking
> seems motivated by the EPTS and similar stuff, which is tracking
> parametricity of arguments, and supports checking-time erasure. The
> matching-on-irrelevant stuff, including this new addition, but also on
> ⊤, ⊥, and the like, is motivated by proof irrelevance, though, which
> supports only closed-term runtime erasure, hence the problem above.
>
> In some cases, it seems safe to do the former's erasure for the latter
> situation. But in general, they are different modalities, and if we
> try to jam them all into one, I think we'll end up with ad-hoc rules
> for how things work. For instance:
>
> data ⊤ : Set where
> tt : ⊤
>
> foo : .⊤ → ℕ
> foo tt = 5
>
> If I normalize 'foo tt', I get 'foo _'. We might decide that it should
> evaluate to 5, and this is safe, but we cannot make a similar decision
> for the identity type, because it will cause my listing above to
> loop... unless we also keep track of what was 'erased' and use it to
> decide whether the irrelevant match in fact matches, and so on.
>
> On Mon, Oct 3, 2011 at 11:13 AM, Andreas Abel<andreas.abel at ifi.lmu.de> wrote:
>> Hi folks,
>>
>> I just pushed a patch that allows one to match on an irrelevant argument,
>> under the proviso that only one constructor matches.
>>
>> The reason why I implemented this feature is because I want to define
>> functions by recursion on a deterministic termination predicate but not
>> prove that its value does not depend on the derivation of that predicate.
>>
>> Please play around with this new feature and find bugs and inconsistencies.
>> ;-)
>>
>> Here is an example (good old division, without sized types, but
>> Bove-Capretta style):
>>
>> module Div where
>>
>> data _≡_ {A : Set}(a : A) : A → Set where
>> refl : a ≡ a
>>
>> data Nat : Set where
>> zero : Nat
>> suc : Nat → Nat
>>
>> minus : Nat → Nat → Nat
>> minus zero m = zero
>> minus (suc n) zero = suc n
>> minus (suc n) (suc m) = minus n m
>>
>> {- definition we'd like to have, does not termination check
>> div : Nat → Nat → Nat
>> div zero m = zero
>> div (suc n) m = suc (div (minus n m) m)
>> -}
>>
>> -- termination predicate
>>
>> data Div! (m : Nat) : Nat → Set where
>> zero : Div! m zero
>> suc : ∀ {n} → Div! m (minus n m) → Div! m (suc n)
>>
>> div' : (n m : Nat) → .(Div! m n) → Nat
>> div' zero m zero = zero
>> div' (suc n) m (suc N) = suc (div' (minus n m) m N)
>>
>> -- irrelevance of termination argument
>>
>> irrDiv! : (n m : Nat)(d d' : Div! m n) → div' n m d ≡ div' n m d'
>> irrDiv! n m d d' = refl
>>
>> Pay attention to the last line!
>> We could have gotten the same result without irrelevance, but much more
>> tedious.
>>
>> Here is another example, involving a universe definition:
>> ( in test/succeed/)
>>
>> module TerminationOnIrrelevantArgument where
>>
>> data ⊥ : Set where
>>
>> data D : Set where
>> empty : D
>> pi : D -> D -> D
>> other : D
>>
>> postulate
>> app : D -> D -> D
>>
>> mutual
>>
>> data Ty : D -> Set where
>>
>> Empty : Ty empty
>>
>> Pi : (a f : D) ->
>> (A : Ty a) ->
>> (F : (d : D) -> .(El a A d) -> Ty (app f d)) ->
>> Ty (pi a f)
>>
>>
>> El : (a : D) -> .(A : Ty a) -> D -> Set
>> El empty Empty g = ⊥
>> El (pi a f) (Pi .a .f A F) g = (d : D) -> .(Ad : El a A d) ->
>> El (app f d) (F d Ad) (app g d)
>> El other () g
>>
>> -- Termination checking needs to look inside irrelevant arguments.
>> -- This only works because the termination checker is syntactic
>> -- and does not respect equality of irrelevant things!
>>
>> -- clearly, the derivation of Ty a does not matter when computing El
>> cast : (a : D)(A A' : Ty a)(d : D) -> El a A d -> El a A' d
>> cast a A A' d x = x
>>
>> 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/
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
--
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