Skip to content

The unbounded fractional authoritative camera

Robbert Krebbers requested to merge robbert/ufrac into master

The unbounded fractional authoritative camera is a version of the fractional authoritative camera that can be used with fractions > 1.

Most of the reasoning principles for this version of the fractional authoritative cameras are the same as for the original version. There are two difference:

  • We get the additional rule that can be used to allocate a "surplus", i.e. if we have the authoritative element we can always increase its fraction and allocate a new fragment.

    ✓ (a ⋅ b) → ●?{p} a ~~> ●?{p + q} (a ⋅ b) ⋅ ◯?{q} b

  • At the cost of that, we no longer have the ◯?{1} a is an exclusive fragmental element (cf. frac_auth_frag_validN_op_1_l).

Edited by Robbert Krebbers

Merge request reports