idempotency of minimzer
Closed this issue · 6 comments
this is hard because the types associated with the derivations aren't the same. one is the input expression, the other is whatever the minimizer returns. it happens to be the point of the theorem that the thing returned is unchanged exactly because the input derivation is subsumption-minimal, but we don't know that statically, so it doesn't type check.
derivations are not a set--in the HoTT sense that just because d1, d2 : Γ ⊢ e => t ~ α ~> e' => t' does not mean that d1 == d2.
so this feels like it's hitting up against the heterogeneous equality problem that Bob's material talks about. you end up wanting to say something holds when transported over something else, but i don't quite know what.
http://jozefg.bitbucket.org/posts/2014-08-06-equality.html good description of hetereogenous equality from Danny, including rude commentary about the great british class system
it's also not idempotency. it's that it's a fixed point for a subset of the input. it's f (x) = x not f(f(x)) = f (x).
Doesn't it suffice to state that minimization gives the same resulting
state? Like it isn't that important that it be the identical derivation.
On Sat, Oct 8, 2016, 23:56 Ian Voysey notifications@github.com wrote:
it's also not idempotency. it's that it's a fixed point for a subset of
the input. it's f (x) = x not f(f(x)) = f (x).—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#34 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AARIPuWRG-TStQX7nF3jNOJwJTTXMt0xks5qyGXggaJpZM4KRkO-
.
I have no idea. They are certainly different things, and I believe both are
true, but one implies the other and not vica versa.
On Sunday, October 9, 2016, Cyrus Omar notifications@github.com wrote:
Doesn't it suffice to state that minimization gives the same resulting
state? Like it isn't that important that it be the identical derivation.On Sat, Oct 8, 2016, 23:56 Ian Voysey <notifications@github.com
javascript:_e(%7B%7D,'cvml','notifications@github.com');> wrote:it's also not idempotency. it's that it's a fixed point for a subset of
the input. it's f (x) = x not f(f(x)) = f (x).—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<https://github.com/hazelgrove/agda-popl17/issues/
34#issuecomment-252463155>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AARIPuWRG-
TStQX7nF3jNOJwJTTXMt0xks5qyGXggaJpZM4KRkO->
.—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
#34 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/AD6MIDBa3m2UeG4GdDem_-MZatnd0VfQks5qyHcFgaJpZM4KRkO-
.
---Ian
done enough for now. see hazelgrove/hazelgrove#15 for future work.