[TYPES] normalization by evaluation for strong sums for STLC

[Neelakantan Krishnaswami]

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 <fdhzs2010 at hotmail.com>
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/
>