1樓：Jason Hu
我一直很想系統地寫一篇這個回答。我趁現在沒啥事我就開個頭吧。
操作語義、指稱語義、代數語義、公理語義學，誰能簡單介紹下？
這裡我都用STLC舉例。
denotational semantics
denotational semantics的原理是找到乙個數學模型，然後證明你的type system是它的乙個模型。我下面給出STLC在agda裡的denotational semantics:
module STLC where
open import Data.Nat
open import Data.List
open import Data.List.Any
open import Data.List.Membership.Propositional
open import Data.Bool
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality
infixr 10 __
data Type : Set where
bool : Type
unit : Type
__ : Type → Type → Type
Env = List Type
typeDenot : Type → Set
typeDenot bool = Bool
typeDenot unit =
typeDenot (s t) = typeDenot s → typeDenot t
wfEnv : Env → Set
wfEnv =
wfEnv (x ∷ env) = typeDenot x × wfEnv env
module Regular where
infixr 10 Λ_
infixl 9 _$$_
infixr 8 LET_IN_
data Term : Env → Type → Set where
var : → T ∈ env → Term env T
true : → Term env bool
false : → Term env boolenv} → Term env unitS T env} → Term (S ∷ env) T → Term env (S TS T env} → Term env (S T) → Term env S → Term env T
LET_IN_ : → Term env S → Term (S ∷ env) T → Term env T
termDenot : → wfEnv env → Term env T → typeDenot T
termDenotfst , _) (var (here refl)) = fst
termDenotTsnd) (var (there x)) = termDenot snd (var x)
termDenot wf truetrue
termDenot wf falsefalse
termDenot wftt
termDenot wf (x $$ ytermDenot wf x (termDenot wf y)
termDenot wf (LET x IN y) = termDenot (termDenot wf x , wf) y
這裡，我把STLC的bool對映到Agda的Bool，unit對映到Agda的，函式對映到Agda的函式。所以我的soundness proof就乙個函式termDenot就做到了。但是，denotational semantics的侷限也比較明顯.
如果你的type system有所謂的impredicative polymorphism，那麼你將無法在formal system裡面構造這種type system的模型。所以你只能做informal proof。
operational semantics
總的來說有兩種，一種叫做big step operational semantics或者evaluation semantics, 另一種叫做small step operational semantics或者structural semantics。前者是從term到value的關係，所以是evaluation；後者則是term到term的，只是一步的reduction。
evaluation semantics一般有如下形式
那麼soudness是證明下面兩個定理：
evaluation semantics有乙個變種就是所謂的definitional interpreter。這時候evaluation semantics是通過乙個函式定義的。那麼這時候第乙個定理就無需證明了。
第二個證明之後通過分析這個函式就可以了。
但是evaluation semantics是有很明顯的侷限性的。這個侷限性在於你必須evaluate到乙個值，這要求你的系統是normalizing的，但這不總是真的，所以small step會更加常見。至於definitional interpreter是更加難用的東西，因為它甚至要求你的operational semantics是deterministic的。
太理想化了，而且證明也很難修改。
structural semantics
是更加常見的operational semantics。它一般有如下形式：
它的soundness是基於Wright and Felleisen 92的progress and preservation:
progress:
preservation:
它的意思是，如果你的term t有一步的reduction，那麼它的型別是不會變化的，這個不停迴圈，到這個term最終變成乙個value為止。
這兩種operational semantics的soundness證明現在不如denotational semantics簡潔。我這裡就不給出了。
categorical semantics
這個semantics是在category theory裡找數學模型。比方說STLC就是cartesian closed category (CCC)的乙個模型。因為我上面給出的stlc帶有乙個bool型別，為了方便，我把對映加強到bicartesian closed category(BiCCC)上。
translation 如下：
這裡，1表示BiCCC的terminal object，1+1表示兩個terminal object的coproduct，剩下乙個是exponential object。所以我給出了STLC是BiCCC的模型的證明。
現今程式語言的理想型別系統是怎樣的？
Jason Hu incompleteness theorem已經決定了程式語言理論裡很多東西都是不可兼得的。難道這個領域還缺乏想把所有事情都做盡結果所有事情都做得一無是處的例子嗎？乙個好的語言應該只有乙個核心理念，做多了的都是假的。 連DT都沒有你說個鬼。Polymorphism不就乙個型別引數，...
如何證明乙個事物是商品？
buyer minds 要證明乙個事物是商品，em.這個用政治經濟學來解釋比較容易。咱們可以看商品的定義，從中匯出證明條件。商品的定義 商品是用於交換的勞動產品，它具有使用價值和價值。這句話說出了商品的四個條件 條件一 可以做交易 不管是拿錢買，拿位元幣買，還是拿東西換，都叫做交易 條件二 勞動的成...
程式設計小白乙個，請問如何系統的學習程式設計，c語言和Python哪個更好
Leon 建議先學習c語言 因為很多語言都是從c語言吸取開發的，可以毫不誇張的說，學好c語言學習其他語言會輕鬆很多，python的語言基礎比起c簡化很多，但是基本想通。都說c語言是開啟程式設計世界的大門 學習族 推薦Python，首先你可以不用在一開始就被各種資料型別和奇葩的報錯困擾，甚至乙個標準讀...