在公理編程中可能性符號Meaning的含義紙

Question

我在閱讀「計算機編程的公理化基礎」。他們在公理中使用可證明符號⊢，例如

⊢P {Q} R 

維基百科描述了使用符號作爲這樣的「X⊢y表示y是從X可證明（在一些指定的正規系統）」，但似乎並不適合這裏。符號是什麼意思？

紙張可以在這裏找到：http://www.cs.ucsb.edu/~kemm/courses/cs266/acmhoare69.pdf

Answer 1

的In x⊢Y，X是一組假設，而y是一個陳述（在你所說的邏輯系統或語言中）。 「x⊢y」表示，在邏輯系統中，如果從假設x開始，可以證明語句y。

因爲x是一個集合，它也可以是空集合。通常這是用空集符號寫成的，但是有時爲了簡潔起見，它完全被遺漏了，這就是發生在這裏的情況。能夠從一套空白的假設證明它意味着它只是真實的（或有效的）。例如，⊢p→p。

Hoare的文章談到了描述程序行爲的語言。正如Todd指出的那樣，「P {Q} R」（用這種語言）是這樣一種陳述，即如果在P爲真的初始狀態下運行程序Q，則R將在事後（如果Q終止）爲真。這是你可能想用一些假設來證明的那種陳述。這些假設將是比初始狀態更高級別的事情：例如，如果您已經證明了一個更簡單但相關的P'{Q'} R'語句，您可能想要假設它證明更大的P {Q } R語句。

因此「P {Q} R」表示語句「P {Q} R」爲真，並且您不需要假設任何內容。

讓我們舉一個簡單的例子。

⊢ X = 3 {Y：= X} x = 3∧Y = 3

我們證明的說法是：「如果x是3時開始，並運行該程序ÿ ：= x，然後x將是3，y將是3.「你不需要任何假設來證明這一點，它來自於語言的定義。你可以繼續使用這個事實作爲假設來證明別的東西。

x = 3 {y：= x} x = 3∧y = 3 ⊢ x = 3 {y：= x; z：= y} x = 3∧y = 3∧z = 3

這裏我們用左邊的簡單語句作爲假設來證明更大的陳述。這是一個非常愚蠢的例子，但我希望它顯示如何閱讀這個。我已經讓⊢大膽地表明它是這條線上的「頂級」事物，將假設與結論分開。左側和右側都是霍爾邏輯中的語句，P {Q} R，其中P和R是邏輯語句，Q是程序。

Answer 2

⊢P {Q} R 

是說， 「P爲程序Q可產生結果R的一個先決條件」