F should be Recognizer_H ∘ Recognizer_M, rather than Recognizer_M ∘ Recognizer_H
In Recognizer_H, I don’t think you can take the expected value of a stochastic term of type SH, because SH doesn’t necessarily have convex structure. But, you could have Recognizer_H output Dist S_H instead of taking the ExpectedValue, and move the ExpectedValue into Win, and have Win output a probability rather than a Boolean.
Confusions:
Your types for Predict_M and Predict_H seem to not actually make testable predictions, because they output the opaque state types, and only take observations as inputs.
I’m also a bit confused about having them take lists of actions as a primitive notion. Don’t you want to ensure that, say, (Predict_M s css (as1++as2)) = (Predict_M (Predict_M s css as1) as2)? If so, I think it would make sense to accept only one action at a time, since that will uniquely characterize the necessary behavior on lists.
I don’t really understand Part1. For instance, where does the variable cs come from there?
Nitpicks:
F should be Recognizer_H ∘ Recognizer_M, rather than Recognizer_M ∘ Recognizer_H
In Recognizer_H, I don’t think you can take the expected value of a stochastic term of type SH, because SH doesn’t necessarily have convex structure. But, you could have Recognizer_H output Dist S_H instead of taking the ExpectedValue, and move the ExpectedValue into Win, and have Win output a probability rather than a Boolean.
Confusions:
Your types for Predict_M and Predict_H seem to not actually make testable predictions, because they output the opaque state types, and only take observations as inputs.
I’m also a bit confused about having them take lists of actions as a primitive notion. Don’t you want to ensure that, say, (Predict_M s css (as1++as2)) = (Predict_M (Predict_M s css as1) as2)? If so, I think it would make sense to accept only one action at a time, since that will uniquely characterize the necessary behavior on lists.
I don’t really understand Part1. For instance, where does the variable
cs
come from there?