真假合金

Question

合金有大量的邏輯連接詞，如and和or和implies。但我找不到true和false。他們是否失蹤？目前我一直在使用1=1和1=0，但這樣做很不方便（並給出編譯器警告）。

_{我的理由，順便說一下，對於希望true和false是我寫的東西，產生.als文件。我的頂級.als文件預計我的自動生成的.als文件定義了一個wellformed謂詞和一個faulty謂詞。有時候這些謂詞很複雜，但有時候我只想讓wellformed[...]返回true，而faulty[...]返回false。這就是爲什麼我需要合金語言中的true和false。}

Answer 1

他們不是建在一個很好的理由：看到軟件抽象（丹尼爾·傑克遜的P137的常見問題， MIT Press，2012）。簡而言之，如果它們是內置的，則必須能夠在布爾值上聲明關係，然後因爲布爾表達式可以評估爲{}和{T，F}，所以連接詞需要是定義這些值，這似乎是一個非常糟糕的主意。

Answer 2

pred true {no none} 
pred false {some none} 

似乎工作;但有這些內置的將是很好的。

Answer 3

由於空謂詞是真實的，我最喜歡的實施真假：

pred true {} 
pred false { not true }