git @ Cat's Eye Technologies The-Dossier / fc986bf
Refine the definition of machine state type (2 sets of locations). Chris Pressey 3 months ago
1 changed file(s) with 39 addition(s) and 19 deletion(s). Raw diff Collapse all Expand all
+39
-19
article/Machine-State-Combinators/README.md less more
323323 Whenever we have a function that takes machine states to machine states, whether it is a
324324 subroutine or a single straight-line instruction or a subprogram, associated with it are:
325325
326 * a set of locations _I_ that the function expects to be meaningful when it
326 * a set of locations **I** that the function expects to be meaningful when it
327327 starts executing,
328 * a set of locations _T_ that it does not guarantee to preserve during its execution, and
329 * a set of locations _O_ (a subset of _T_) that it warrants to be meaningful after its
328 * a set of locations **C** that it does not guarantee to preserve during its execution, and
329 * a set of locations **O** (a subset of **C**) that it warrants to be meaningful after its
330330 execution has finished.
331331
332 All location that are not in _T_, after the execution, are guaranteed to not have
333 changed (something like a frame axioms). The locations in _T_ have no such guarantee,
334 but their subset _O_ are guaranteed to be meaningful.
332 All location that are not in **C**, after the execution, are guaranteed to not have
333 changed (something like a frame axioms). The locations in **C** have no such guarantee,
334 but their subset **O** are guaranteed to be meaningful. The set
335 **C** - **O** can be referred to as a **T** ("trashed"). By the same
336 token, **C** = **O** ∪ **T**.
337
338 If there are meaningful locations in **I** that are outside **C**,
339 they will remain meaningful in the result, as indeed, they remain
340 unchanged in the result.
335341
336342 So the type `P` is really more like
337343
338 S[I] ->[T] S[O]
344 S[I] -> S[O]
339345
340346 where `I` corresponds to `M1` (the set of machine locations which we required
341 to be meaningful in the input state), `O` corresponds to `M2` (the set of machine
342 locations which we warrant to be meaningful in the output state), and `T` is part of
343 the function type itself, and defines the "frame" in which the program operates.
347 to be meaningful in the input state), and `O` corresponds to `M2` (the set of machine
348 locations which we warrant to be meaningful in the output state).
344349
345350 Machine state types have a notion of compatibility here, which is not manifest in
346351 the `S[M1] -> S[M2]` example.
347352
348 If _f_ is a function of type `S[I] ->[T] S[O]`, then _f_ can be applied to any machine
353 If _f_ is a function of type `S[I] -> S[O]`, then _f_ can be applied to any machine
349354 state that is _at least as meaningful as_ `S[I]` - that is, any machine state `S[X]`
350 where I ⊆ X.
351
352 We might informally say _f_ will "throw away" the extra meaningfulness in X. Given that
353 we know `T` and `O`, we know exactly what it will throw away, too - everything in X that
354 is in T and not in O (or more formally: X ∩ T - O).
355
356 If we try to apply _f_ to `S[Y]` where Y ⊆ I, that is a type error, because `S[Y]` does
357 not have machine locations in its set of meaningful locations, that _f_ requires to be
355 where **I** ⊆ **X**.
356 We might informally say _f_ will "throw away" any extra meaningfulness in **X**.
357
358 If we try to apply _f_ to `S[Y]` where _Y_ ⊆ **I**, that is a type error, because `S[Y]` does
359 not have the machine locations in its set of meaningful locations, that _f_ requires to be
358360 meaningful.
361
362 Where does **C** fit in? Well, our state type expresses meaningfulness;
363 we need to extend it to to express unmeaningfulness too. Something
364 like this:
365
366 S[I, T.in] -> S[O, T.out]
367
368 The second parameter of our type here is the set of machine locations
369 in the machine state which we deem unmeaningful.
370
371 Any location which is in **T.in**, i.e. unmeaningful in the input,
372 must either appear in **T.out**, i.e. be unmeaningful in the output,
373 or in **O**, i.e. it was set by the function as a meaningful output.
374
375 So to recap, our `S` type is actually `S[M,U]`, parameterized by
376 two sets of machine locations: the machine locations that are
377 deemed to be meaningful (`M`) and the machine locations that are
378 deemed to be unmeaningful (`U`) in that machine state.