The subtler issue is that it's a counterfactual question. What would have happened if I had measured or been able to measure all three angles 0, a, 2a? In this case the bit string is the same except for the 1% difference. In other words, X(t) = Y(t), for all t.
The argument is essentially trying to construct a "hidden variable" model and showing that it can't work.
This is blatantly false. People are using formal verification tools in hardware design, and they do work and they do compose. Here is a simple verilog code which accomplishes some of what he wants.
module Blinker (
input wire clock,
output reg state
);
always @(posedge clock)
state <= !state;
`if FORMAL
always @(posedge clock)
assert ($past(state) != state);
`endif
endmodule
module testbench (
input wire clock,
output wire state1,
output wire state2
);
Blinker blinker1(clock, state1);
Blinker blinker2(clock, state2);
`if FORMAL
# assume that they are different
assume (state1 != state2);
# then they stay different
always @(posedge clock)
assert (state1 != state2);
`endif
endmodule
Of course you NEED clock wires to the blinker. Composability comes from the use of assume and assert. You assume that your environment is behaving according to spec and you prove that you are also behaving to spec PROVIDED the environment working correctly. See https://symbiyosys.readthedocs.io/en/latest/index.html for more details.
Moral of the story: broken spec cannot be used, and I am saying this as a mathematician!
This. We use Hoare logic verification in software in very similar ways, to assert on symbol intervals to make sure arithmetic and memory operations can succeed in e.g. C.
I am a researcher, and I fail to find detailed data, please help! In all datasets we see cumulative confirmed, recovered and death numbers organized by day. We would need culumative confirmed by onset time (first symptoms), and confirmed by test time (the current value). We would also need recovered and death by onset time and confirmation time. Where are these numbers?
Unfortunately the existing public data sets I've seen lack this information. The level of detail for each confirmed case is largely dependent on which country is reporting the data (plus it's often in an unstructured and inconsistent format). I would love to know if you find any data source with more details.
You can use the tensor formalism to express combinatorial problems, but these will not be smooth, so gradient descent algorithms will not work. However, you can turn such boolean tensor problems into huge SAT problems and solve them with SAT solvers. See for example here: https://github.com/mmaroti/uasat
X(0) = 0000, Y(a) = 0001, X(a) = 0011, Y(2a)= 0111.