git @ Cat's Eye Technologies
Fix disjunction-involving-bottom laws. Chris Pressey 1 year, 14 days ago
1 changed file(s) with 9 addition(s) and 1 deletion(s).
 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 --------------------