Optimization of act/run in #270.

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Apache License 2.0

205 stars 12 forks source link

Optimization of act/run in #270. #352

Closed favonia closed 6 years ago

favonia commented 6 years ago

@jonsterling There are two optimizations of act/run I regard as essential in the new domain:

[x] The run phi2 should be completely "dropped" in run phi1 @@ run phi2 m.
[x] If m is already a phi-value, run phi m should be a no-op as much as possible.

I know how to do optimization 1 when working with faces, and I wonder if optimization 0 was already implemented in #270?

jonsterling commented 6 years ago

Thanks for the Thought, I agree. A couple comments:

I think I know how to mostly implement (0), by replacing recursive calls to run with one of those explicit re-indexings M_\Xi or whatever.
I am not sure how to achieve optimization (1). Can you unleash some thoughts about that?

favonia commented 6 years ago

2. I am not sure how to achieve optimization (1). Can you unleash some thoughts about that?

When working with faces, if the cofibration ri = ri' is already true (which could happen for boundaries of neutral values), drop phi (and do whatever neccesary).

favonia commented 6 years ago

Implemented some optimization 1 in #270 by 8eff62b.

jonsterling commented 6 years ago

@favonia Why is it justified to drop phi in that case? Do we somehow know that if ri = ri', then the restriction is already stronger than phi? I don't quite understand.

favonia commented 6 years ago

@favonia Why is it justified to drop phi in that case? Do we somehow know that if ri = ri', then the restriction is already stronger than phi? I don't quite understand.

You're right. I'll fix that.

favonia commented 6 years ago

Done it the current PR #270.