Difference between revisions of "Probabilistic Soundness"

From GM-RKB
Jump to: navigation, search
Line 27: Line 27:
  
 
=== 2015b ===
 
=== 2015b ===
* ([[2015_ProbabilisticTerminationSoundne|Ferrer Fioriti & Hermanns, 2015]]) ⇒ [[author::Luis María Ferrer Fioriti]], and [[author::Holger Hermanns]]. ([[year::2015]]). “[https://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf Probabilistic Termination: Soundness, Completeness, and Compositionality].” In: [[Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages]]. ISBN:978-1-4503-3300-9 [http://dx.doi.org/10.1145/2676726.2677001 doi:10.1145/2676726.2677001]  
+
* ([[2015_ProbabilisticTerminationSoundne|Ferrer Fioriti & Hermanns, 2015]]) ⇒ [[::Luis María Ferrer Fioriti]], and [[::Holger Hermanns]]. ([[::2015]]). “[https://www.ae-info.org/attach/User/Hermanns_Holger/Publications/FH-POPL15.pdf Probabilistic Termination: Soundness, Completeness, and Compositionality].” In: [[Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages]]. ISBN:978-1-4503-3300-9 [http://dx.doi.org/10.1145/2676726.2677001 doi:10.1145/2676726.2677001]  
** QUOTE: '''Theorem 5.6 (Soundness).''' Let P be a [[probabilistic program]] with [[semantics]]] {(L, X) φ n}, and a [[ranking]] [[supermartingale]] {Yn} such that Yn = 0 implies T φ ≤ n for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.
+
** QUOTE: <B>Theorem 5.6 (Soundness).</B> Let <math>P</math> be a [[probabilistic program]] with [[semantics]]] <math>{(L, X) φ n}</math>, and a [[ranking]] [[supermartingale]] <math>{Y_n}</math> such that <math>Y_n = 0</math> implies <math>T φ ≤ n</math> for all valid schedulers φ. Then, P almost sure terminates, and T ∗ is integrable.
  
 
=== 2009 ===
 
=== 2009 ===
Line 35: Line 35:
  
 
=== 1975 ===
 
=== 1975 ===
* (Adams, 1975) ⇒ E. W. Adams (1975). [http://fitelson.org/piksi/adams_logic_of_conditionals.pdf "The logic of conditionals: An application of probability to deductive logic"] (No. 86). Springer Science & Business Media.
+
* ([[Adams, 1975]]) ⇒ E. W. Adams (1975). [http://fitelson.org/piksi/adams_logic_of_conditionals.pdf "The logic of conditionals: An application of probability to deductive logic"] (No. 86). Springer Science & Business Media.
 
** QUOTE: Our objective as this section is to establish a <i>prima facie</i> case for the appropriateness of assessing the [[soundness]] or [[rationality]] of [[deductive inference]]s in terms of a new requirement or [[criterion of rationality]] beyond the usual [[truth-conditional criterion]]: that it should be impossible for the [[premise]]s of an [[inference]] to be true while its [[conclusion]] is false. The proposed supplementary [[criterion]] results when the words 'probable` and 'improbable' are substituted for 'true' and 'false', respectively, in the [[truth-conditional criterion]], yielding the <i>[[probabilistic soundness criterion]]</i>: it should be impossible for the [[premise]]s of an [[inference]] to be [[probable]] while its [[conclusion]] is improbable. This [[formulation]] is vague and we shall want to clarify it later, but our present concern is with the legitimacy of demanding that [[deductive inference]]s satisfy something like this requirement if they are to be regarded as 'rational'.  
 
** QUOTE: Our objective as this section is to establish a <i>prima facie</i> case for the appropriateness of assessing the [[soundness]] or [[rationality]] of [[deductive inference]]s in terms of a new requirement or [[criterion of rationality]] beyond the usual [[truth-conditional criterion]]: that it should be impossible for the [[premise]]s of an [[inference]] to be true while its [[conclusion]] is false. The proposed supplementary [[criterion]] results when the words 'probable` and 'improbable' are substituted for 'true' and 'false', respectively, in the [[truth-conditional criterion]], yielding the <i>[[probabilistic soundness criterion]]</i>: it should be impossible for the [[premise]]s of an [[inference]] to be [[probable]] while its [[conclusion]] is improbable. This [[formulation]] is vague and we shall want to clarify it later, but our present concern is with the legitimacy of demanding that [[deductive inference]]s satisfy something like this requirement if they are to be regarded as 'rational'.  
----
+
 
 
----
 
----
  
 
__NOTOC__
 
__NOTOC__
 
[[Category:Concept]]
 
[[Category:Concept]]

Revision as of 04:51, 14 June 2019

A Probabilistic Soundness is a Rationality Criterion that ...



References

2019

  • (Wikipedia, 2019) ⇒ https://en.wikipedia.org/wiki/Probabilistically_checkable_proof#Definition Retrieved:2019-6-14.
    • Given a decision problem L(or a language L with its alphabet set Σ), a probabilistically checkable proof system for L with completeness c(n) and soundness s(n), where 0 ≤ s(n) ≤ c(n) ≤ 1, consists of a prover and a verifier. Given a claimed solution x with length n, which might be false, the prover produces a proof π which states x solves L (xL, the proof is a string ∈ Σ*). And the verifier is a randomized oracle Turing Machine V (the verifier) that checks the proof π for the statement that x solves L(or xL) and decides whether to accept the statement. The system has the following properties:
      • Completeness: For any xL, given the proof π produced by the prover of the system, the verifier accepts the statement with probability at least c(n),
      • Soundness: For any xL, then for any proof π, the verifier mistakenly accepts the statement with probability at most s(n).

2015a

2015b

2009

1975