urbit/ares
1
1
Fork 0
mirror of https://github.com/urbit/ares.git synced 2024-11-22 06:32:47 +03:00
Code Issues Packages Projects Releases Wiki Activity

Make crash-agnosticism explicit

Browse Source
This commit is contained in:
Edward Amsden 2022-03-30 20:00:41 -04:00 committed by GitHub
parent 6f5e567a10
commit bc3540eb76
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
docs/subject-knowledge.md
View File

@ -47,6 +47,11 @@ This may seem counterintuitive, but the algorithm describes how this knowledge i
The Nock primitives `/[a b]` and `#[[a b] c]` extend to socks in the obvious way, giving a crash when it can be *known* that the computation would crash, e.g. when attempting to access a non-1 axis of an atom, or
when an axis is not an atom.
Note that while Subject Knowledge Analysis can often determine that a computation *will* crash, it cannot presently determine that a computation *will* not crash.
Thus, the knowledge of the result of a computation is knowledge of the result assuming the computation does not crash.
Thus, for instance, knowledge of the result of `4` where the subformula result is `[%gues ~]` is `[%dice ~]`, despite the fact that the subformula could produce a cell and cause the computation to crash.
Put another way, so long as a `4` does not crash, it will always produce an atom, and thus the knowledge produced is `[%dice ~]`.
### Cell
SKA of a cell formula applies the analysis to both formulae with the same subject knowledge input, then combines their inputs into a `%bets` cell and normalizes the result.