git @ Cat's Eye Technologies Tandem / 0.1
Fix disjunction-involving-bottom laws. Chris Pressey 4 years ago
1 changed file(s) with 9 addition(s) and 1 deletion(s). Raw diff Collapse all Expand all
+9
-1
README.md less more
33 _Wiki entry_ [@ esolangs.org](https://esolangs.org/wiki/Tandem)
44 | _See also:_ [Squishy2K](https://github.com/catseye/Squishy2K)
55 ∘ [Strelnokoff](https://github.com/catseye/Strelnokoff)
6 ∘ [Cabra](https://github.com/catseye/Cabra)
67 ∘ [Arboretuum](https://github.com/catseye/Arboretuum)
78 ∘ [Tamsin](https://github.com/catseye/Tamsin)
89
310311
311312 For conjunction, ⊥ & R = R & ⊥ = ⊥. This is intuitively justified.
312313
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.
314318
315319 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).)
316324
317325 Algebraic properties
318326 --------------------