fact（已知的事實）與 rule（能從事實推導新事實的規則）。先宣告一個輸入關係，代表「模組a直接相依於模組b」

// 代表 a 直接 import b
.decl depends(a: symbol, b: symbol)
.input depends

.decl 宣告關係的名字與各欄位型別（symbol 是字串，另一個常用型別是 number）。.input 表示資料從外部讀入：預設是從同名的 depends.facts 檔案，每行一筆、以 Tab 分隔。接著我們定義第一條規則：模組若被任何人相依，就是「被使用的」

.decl used(m: symbol)
used(m) :- depends(_, m).

讀法是「對任意 m，若存在 depends(_, m)，則 used(m) 成立」。:- 右邊是body（前提），左邊是head（結論），_ 是 wildcard，表示「有就好、是誰都可以」。開發者不用管理控制流程：規則評估結果是順序無關的，由引擎自己算出所有成立的結論

Datalog的威力來自join，同一個變數出現在多個atom裡時，概念上是約束成同一個，會觸發unification。比如「a透過某個中介x間接相依於b」可以寫成

.decl indirect(a: symbol, b: symbol)
indirect(a, b) :-
  depends(a, x),
  depends(x, b).

x 在兩個 depends 裡都出現，引擎就通過「a依賴的東西」和「依賴b的東西」計算a到b的間接依賴

但 indirect 只有 a -> b -> c 的情況會被辨識出來，相依是會傳遞的，不論中間隔幾層，可達性是經典的遞迴關係：transitive closure

.decl reachable(a: symbol, b: symbol)
reachable(a, b) :- depends(a, b).
reachable(a, b) :-
  depends(a, x),
  reachable(x, b).

• base case：直接相依就是可達
• induction case：a 依賴 x，x 遞迴可達的所有 b 都是 a 可達的

這裡的 reachable 只在 depends 既有的symbol之間關聯，不發明新值，可推導的fact是有限集，所以一定收斂

但保證終止不是Soufflé的通則。它有算術functor，只要規則會合成新值（如 A(i + 1) :- A(i).），domain就變成無限，會產生無窮迴圈，這種情況要自己加 i < 10 之類的條件控制

有了可達性，就能問「哪些模組是死碼」：不是從entry point可達的模組。這需要negation。先標出進入點，再定義「可從某entry到達」

.decl entry(m: symbol)
.input entry

.decl live(m: symbol)
live(m) :- entry(m).
live(m) :-
  entry(e),
  reachable(e, m).

.decl dead(m: symbol)
.output dead
dead(m) :-
  depends(m, _),
  !live(m).
dead(m) :-
  depends(_, m),
  !live(m).

!live(m) 是negation。Datalog的negation必須是 stratified（分層）的——不能有「自己依賴自己的否定」這種循環。Soufflé會把程式分層，確保 live 在被否定使用前已完全算完，!live 的語意才有良好定義

Datalog不只能推導關係，也能做聚合。例如算出每個模組「被多少人直接相依」，找出最該謹慎修改的核心

.decl fan_in(m: symbol, n: number)
.output fan_in
fan_in(m, n) :-
  used(m),
  n = count : { depends(_, m) }.

count : { depends(_, m) } 是「滿足 depends(_, m) 的fact有幾筆」。對固定的 m，引擎算出有多少個模組相依於它，綁定 n。Soufflé 也提供 max、min、sum，語法相同。聚合讓我們不必跳出Datalog就能回答「最多、最少、總共」這類問題

把上面的規則存成 deps.dl，準備一個 facts/ 目錄放輸入：depends.facts 每行一筆 模組A⟨tab⟩模組B；entry.facts 列出進入點。然後在shell中輸入

souffle deps.dl -F facts -D out

-F 指定fact目錄，-D 指定輸出目錄。每個標了 .output 的關係跑完都會出現在 out/ 下：out/dead.csv 是deadcode的清單，out/fan_in.csv 是各模組的被依賴數量

以上是直譯模式，開發時使用。資料量大、要追求速度時，可以把程式編成原生執行檔再跑

souffle -o deps deps.dl
./deps -F facts -D out

理論部分參考 On Fast Large-Scale Program Analysis in Datalog

Soufflé的心智模型很單純：我們描述「什麼成立」，引擎反覆套用推理規則直到不動點，算出所有能推導的facts

它的優勢在「對大量結構化資料反覆做join與遞迴查詢」：程式分析（points-to、call graph、taint）、相依與可達性分析、各種圖上的規則推導。當問題能轉換成「一組fact加一組蘊含式」，Soufflé就能精簡的表示邏輯，又不用損失執行速度