Basic questions: If the type of Adv(M) is a pseudo-input, as suggested by the above, then what does Adv(M)(x) even mean? What is the event whose probability is being computed? Does the unacceptability checker C also take real inputs as the second argument, not just pseudo-inputs—in which case I should interpret a pseudo-input as a function that can be applied to real inputs, and Adv(M)(x) is the statement “A real input x is in the pseudo-input (a set) given by Adv(M)”?
(I don’t know how pedantic this is, but the unacceptability penalty seems pretty important, and I struggle to understand what the unacceptability penalty is because I’m confused about Adv(M)(x).)
Basic questions: If the type of Adv(M) is a pseudo-input, as suggested by the above, then what does Adv(M)(x) even mean? What is the event whose probability is being computed? Does the unacceptability checker C also take real inputs as the second argument, not just pseudo-inputs—in which case I should interpret a pseudo-input as a function that can be applied to real inputs, and Adv(M)(x) is the statement “A real input x is in the pseudo-input (a set) given by Adv(M)”?
(I don’t know how pedantic this is, but the unacceptability penalty seems pretty important, and I struggle to understand what the unacceptability penalty is because I’m confused about Adv(M)(x).)
The idea is that we’re thinking of pseudo-inputs as “predicates that constrain X” here, so, for α∈Xpseudo, we have α:X→B.
Ah right, thanks! (My background is more stats than comp sci, so I’m used to “indicator” instead of “predicate.”)