[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi, You probably want Sam Lindley's *Extensional Rewriting with Sums*, TLCA 2007. https://homepages.inf.ed.ac.uk/slindley/papers/sum.pdf He calls the equation you give as the "move-case" rewrite. Best, Neel On Tue, Mar 30, 2021, 6:26 AM Jason -Zhong Sheng- Hu <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > Hi all, > > I am trying to find papers on NbE algorithms handling strong sums for > STLC. In particular, I want to see how this commuting conversion rule is > dealt with: > > (match t with > | inl y => s > | inr z => u) t' > ============> > match t with > | inl y => s t' > | inr z => u t' > > that is, applications immediately after a pattern matching are distributed > into the branches. > > For most papers I found, they only deal with either other commuting > conversions or eta for sums. I am aware of > https://ieeexplore.ieee.org/document/932506 which does handle that > commuting conversion in interest, but it is too category-heavy. I am > looking for more light-weight semantic methods. Is there any other method > to deal with strong sums which I am not aware of? > > Thanks, > Jason Hu > https://hustmphrrr.github.io/ >
