id: 3e4afb8780454d6da1c1936713c1fdfe
parent_id: d53d8019868a460ca4dbf7ed2f615a7f
item_type: 1
item_id: fc9e4d47857b4515a6b6531b36cf3691
item_updated_time: 1683574776615
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\"s.\\\n\\\n\"],[-1,\"Meng and Paulson talk, in their discussion of HOL translations, about the soundness of proofs. They say \\\"omitting types yields a compact result, but the resulting proofs can be _unsound_: that is, meaningless in higher-order logic.\\\" For instance, take the context and conjecture:\\\n\\\ndatatype two = a | b\\\nh : forall(x: two, x = a \\\\/ x = b)\\\n|- forall(x: nat, x = a \\\\/ x = b)\\\n\\\nThis is obviously false (in fact, not even well-typed). However, if we erase types:\\\n\\\nh : forall(x, x = a \\\\/ x = b)\\\n|- forall(x, x = a \\\\/ x = b)\\\n\\\nNow, our hypothesis is equal to our goal, and our proof is trivial. This proof is, however, \\\"unsound\\\", in the sense that it is a proof of something that is not true in the original logic.\\\n\\\nThe authors also discuss the soundness of translations. For instance, they call the fully-typed translation \\\"sound\\\", meaning that it does not produce problems that admit unsound proofs.\\\n\\\nNow, in the Encoding Monomorphic and Polymorphic Types paper, we get the following definitions of \\\"sound\\\" and \\\"complete\\\" translations:\\\n\\\n\\tA translation that translates problems Phi over signature Sigma to Phi' over Sigma' is _sound_ if the satisfiability of Phi implies the satisfiability of Phi'.\\\n\\t\\\nNow, this seems to me the exact opposite. This precludes our translation from making problems unsatisfiable, but that is not of primary importance to us. What we care about is that, once we have a proof in our target logic, that tells us something about the existence of a proof in our source logic. That is, if Phi' is satisfiable, so is Phi. This property they call \\\"completeness\\\", but MePo call such a proof \\\"sound\\\".\\\n\\\nHmm, actually, I think this might me a consequence of me mixing up \\\"x has a proof\\\" and \\\"x is satisfiable\\\".\\\n\\\nMePo talk about a sound translation as if it means\\\n\\\nM' |- phi' => M |- phi\\\n\\\nBut Blanchette et al. define it as\\\n\\\nM |= phi => M' |= phi'\\\n\\\nThat is, satisfiable problems in the source logic are satisfiable in the target logic.\\\n\\\n\"],[1,\"In the Encoding Monomorphic and Polymorphic Types paper, we get the following definitions of \\\"sound\\\" and \\\"complete\\\" translations:\\\n\\\n\\tA translation that translates problems Phi over signature Sigma to Phi' over Sigma' is _sound_ if the satisfiability of Phi implies the satisfiability of Phi'.\\\n\\t\"],[0,\"\\\n## \"]],\"start1\":3814,\"start2\":3814,\"length1\":1953,\"length2\":301}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-05-08T19:48:48.304Z
created_time: 2023-05-08T19:48:48.304Z
type_: 13