Fix disjunction-involving-bottom laws.
Chris Pressey
1 year, 14 days ago

3 | 3 | _Wiki entry_ [@ esolangs.org](https://esolangs.org/wiki/Tandem) |

4 | 4 | | _See also:_ [Squishy2K](https://github.com/catseye/Squishy2K) |

5 | 5 | ∘ [Strelnokoff](https://github.com/catseye/Strelnokoff) |

6 | ∘ [Cabra](https://github.com/catseye/Cabra) | |

6 | 7 | ∘ [Arboretuum](https://github.com/catseye/Arboretuum) |

7 | 8 | ∘ [Tamsin](https://github.com/catseye/Tamsin) |

8 | 9 | |

310 | 311 | |

311 | 312 | For conjunction, ⊥ & R = R & ⊥ = ⊥. This is intuitively justified. |

312 | 313 | |

313 | For disjunction, ⊥ | R = ⊥ (if the first rule matched) or R (if the second rule matched); if both rules matched it was a runtime error (which we could also think of as ⊥, but anyway let's not go there quite yet). | |

314 | For disjunction, ⊥ | R = R | ⊥ = ⊥. This is justified by the observation that, in order to know if both Ri and Rj match (which | |

315 | would be a runtime error (which we could also think of as ⊥, but anyway let's not go there quite yet)) we must, in essence, | |

316 | speculatively execute both Ri and Rj, and during this speculative execution, it is possible that one or both of them will | |

317 | fail to terminate, meaning that their disjunction will also fail to terminate. | |

314 | 318 | |

315 | 319 | For asteration, ⊥\* = ⊥. |

320 | ||

321 | (I think the laws for ⊥ do not lead to the algebraic structure becoming inconsistent — but if they do, | |

322 | we needn't feel the least guilty about it, as we are informed that | |

323 | [fast and loose reasoning is morally correct](https://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf).) | |

316 | 324 | |

317 | 325 | Algebraic properties |

318 | 326 | -------------------- |