Deciding to use a lambda for `wrong` or not in `one`

[rogerburtonpatel]

Which of the two translations to one in https://github.com/rogerburtonpatel/vml/blob/main/tex/translations/cond-desugar.pdf appeals to you? Why?

[nrnrnr]

In both translations, I don't see why $e_g$ is a guarded-exp and not just an exp.

I was surprised that the second translation is not inductive.

Neither translation lends the insight I was hoping for.

For writing translations I recommend the Oxford brackets, which you may remember from 106: ⟦̣⋯⟧. Often preceded by a translation function, as in 𝒯⟦̣⋯⟧.

Direct rewrite rules for if e₁ [] e₂ [] ⋯ [] eₙ fi, where each eᵢ is a guarded-exp, might lend more insight.

ETA: I don't think it matters where you put wrong. Both placements work.

[rogerburtonpatel]

Thank you for your insight!

In both translations, I don't see why eg is a guarded-exp and not just an exp.

I interpreted this to mean: if-fi's branches are guarded_exp -> exp, or just guarded_exp, depending on which definition you use. But with cond we're still in uML land, so it should just be exp. Is this what you meant?

I was surprised that the second translation is not inductive.

Fixed it to be inductive.

Neither translation lends the insight I was hoping for.

shame

For writing translations I recommend the Oxford brackets, which you may remember from 106: ⟦̣⋯⟧. Often preceded by a translation function, as in 𝒯⟦̣⋯⟧.

Good call-- thank you. Now using.

Direct rewrite rules for if e₁ [] e₂ [] ⋯ [] eₙ fi, where each eᵢ is a guarded-exp, might lend more insight.

I'll add these in if-fi-rewrite.pdf tomorrow.

ETA: I don't think it matters where you put wrong. Both placements work.

Got it. I prefer the one with wrong without the lambda- it works more cleanly into an inductive translation. It can also save a function application in optimization to have wrong without the lambda- not something I'll spend time thinking about right now!

[rogerburtonpatel]

Please feel free to add anything for this ^ and then close the issue.