Timeline for What is hereditary substitution and why should I use it?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 30, 2022 at 12:53 | comment | added | Jonathan Sterling | Related to the work of Arbob and Bob, there is also some similar subsequent work by Munch-Maccagnoni and Scherer: hal.inria.fr/hal-01160579. | |
| Mar 30, 2022 at 10:52 | comment | added | Neel Krishnaswami | Note how the commuting conversion pushes $f$ into the branches and duplicates it. | |
| Mar 30, 2022 at 10:51 | comment | added | Neel Krishnaswami | Yes: $f(b) \triangleq \mathsf{if}\,b\,\mathsf{then}\,f(\mathsf{true})\,\mathsf{else}\,f(\mathsf{false})$ | |
| Mar 29, 2022 at 19:05 | comment | added | Ms. Molly Stewart-Gallus | @NeelKrishnaswami No later I realized it isn't a full solution. You have reduced the problem to eta expanding tags. But do you eta expand boolean values? | |
| Mar 29, 2022 at 12:58 | comment | added | Neel Krishnaswami | @MolossusSpondee: that totally works! In my comment I meant coproduct types when I wrote sum. They require the ability to branch, and have pattern-matching-style eliminators with a complex set of commuting conversions. | |
| Mar 28, 2022 at 17:43 | comment | added | Ms. Molly Stewart-Gallus | Thinking about the eta expansion for a dependent sum like encoding of sum types. Something like $\langle \textbf{tag} \mathrel{:=} \pi_1 e, \pi_2 e \rangle$ Not sure why that doesn't work | |
| Mar 28, 2022 at 11:03 | comment | added | Neel Krishnaswami | WMM = Workshop on Mechanising Metatheory | |
| Mar 28, 2022 at 11:01 | comment | added | Neel Krishnaswami | If memory serves, Arbob Ahmed and Bob Harper worked out a focusing-based normal-forms presentation for sums in WMM 2007. The idea was to use multifocusing plus variable ordering (a la BDDs) to get unique normal forms. Unfortunately this was never properly published. | |
| Mar 28, 2022 at 9:09 | comment | added | András Kovács | I made no claim about practical feasibility, only about feasibility of formalization in OP's desired quotient/conversion-free style. | |
| Mar 28, 2022 at 9:04 | history | answered | Neel Krishnaswami | CC BY-SA 4.0 |