1. 程序代數
所以，用一些形式語言說明規則系統的架構。推論引擎包含三個分開的程序，所以我們用到基本程序代數(Pi Calculus)：令 p, q 是二個程序，二個程序的結構可能是下列其中一種樣子。
p, q ::= a(c) . p (輸入)
| a! c . p (輸出)
| a! c . p (輸出)
| P | q (平行處理)
| if x = y then p else q (條件控制)
| rec z . p (遞迴)
| stop (終止)
上述項目的意義是：
- a(c) . p 是程序 p 要從 a 通訊管道取得一些資料 c ；
- a! c . p 是程序 p 要對 a 通訊管道送出一些資料 p ；
- p | q 是二個程序 p, q 平行地執行；
- if x = y then p else q 是先比較二項資料 x 和 y ，如果 x = y 就執行程序 p ，否則執行程序 q ；
- rec z . p 是將程序 p 定義為一個遞迴程序，以 z 標示。在 p 中存在 z 符號，表示遞迴呼叫；
- stop 是一個終止程序。
我們說， P <= a(b) . p 是定義一個程序 P 的內容是， p 知道一 通訊管道 a 並 管道 a 取出資料
b 。為了方便，用 P(a) 表示此式，即程序 P 一開始就知道通訊管道 a ，並可以隨意使用。
2. 基本詞彙
另外，我們需要一些基本符號，列舉如下：
單元詞彙：要表示一個資料單位或一項物件，用小寫字母 a, b, ..., z 表示任何一個單元。
集合詞彙：用大寫字母 A, B, ..., Z 表示任何一個集合。每一個集合中包含了許多單元。所以，x ＜ X 表示一個單元詞彙 x 屬於另一個集合 X 。
邏輯式或敘述：用一些單元詞彙和一些邏輯運算符號 & , | , ~ , -> 等等，組合成另一些字串，這些字串稱為邏輯式、或稱為敘述：例如，有單元詞彙 x, y ，則 x & y 是一則敘述、 ~x 是一則敘述、並 (x & y -> x) | (x & y -> y) 也是一則敘述。在本篇文章，我們要用到許多 -> 運算符號。
隱含( -> )：是一種邏輯運算符號，用來表示符號的左項和右項之間有因果關係：例如，對單元詞彙 x, y 來說， x -> y 是一則敘述，其意義是
x y x -> y
true true true
true false false
false true true
fase false true
只有當 x 有效但 y 無效時， x -> y 不能成立。這稱為「 x 隱含 y 」、「 x 代表 y 」。
例外詞彙：任何其他用途的詞彙，都用粗體大寫字母 A, B, ..., Z 表示：例如，用 M 表示一則程序。
Lambda函數：是一種匿名函數的表示法，以格式為「 入 a b c ... . p(a, b, c, ...) 」的字串表示一則函數。其中，「入」是希臘文字母，唸 lambda ；「入」之後是一些參數、之後是一點、之後是函數內容：例如， 入x y . x + y 是一則匿名函數，接受二項參數而計算總和。
3. 定義
事實：用一個單元詞彙表達一項事實：例如，用 x 表達「今天下雨」。
規則：用一則格式為「 a & b & ... -> a & b & ... 」的邏輯式，表示一條規則：例如 a & b -> c & d 。其中， -> 符號左邊稱為左手側，常用英文 LHS 表示；右邊稱為右手側，常用英文 RHS 表示。左手側就是規則條件，而右手側就是規則的結論。
規則系統：是一組結構 ＜F, R, M, C, A ＞ ，其中組成單元有：
- F ：一些事實的集合。
- R ：一些規則的集合。
- M ：規則比對程序，負責將一些事實和一些規則彼此比對，然後選出符合比對的規則，當做結果。
- C ：協調程序，負責將 M 的結果做衝突協議(Conflict Resolution)。衝突協議是在一些規則中，只挑選一些必須啟動的規則，當做結果；並排除彼此衝突或互相重覆的規則：例如，規則 A & B -> C 和規則 A -> C 重覆，因為前者的規則條件是後者的子集合。 Rete 演算法規定，對這二條規則，要選擇 A & B -> C ，因為規則條件比較嚴格。
- A ：行動程序，負責將 C 的結果── 一些確定要啟動的規則 ──確實執行。 A 要將 C 結果的右手側取出並執行。
Rete 結構： Rete 演算法是討論一些規則的集合應該如何組織、並組織一種有效的結構，使事實和規則彼此比對變的比較有效。令有一些規則為 R = { A & B -> C , B & C -> D } ，根據最初的 Rete 演算法論文， R 有一組對應的 rete 結構，令為 R(R) 。 R(R) 包含一些流程控制，定義為
入 f . R(R) ::=
入 f . if type(f) = A then assert(C(_^B)) ;
if type(f) = B then assert(C(A^_)); assert(D(_^C)) ;
if type(f) = C then assert(D(B^_)) ;
if assert(C(_^B)) and assert(C(A^_)) then match(A & B -> C) ;
if assert(D(_^C)) and assert(C(B^_)) then match(B & C -> D)
在 R(R) 中由三種節點構成，包括 type(f) = A 檢查輸入事實的 type 屬性、 assert(C(A^B)) 表示結果 C 是由 A & B 決定、以及 match(r) 指明條件 r 已經符合比對。而 C(_^B) 表示 C 的一則決定項已經接受、並等待另一則決定項 B 。
4. 推論引擎
推論引擎包含 M, C, A 三項程序，依序循環使用。我們用程序代數和上述符號標記法定義三項程序。
取比對程序 M 為
M(a, b) <= rec z . a(f1, (f2, f*)) . ((入 f . R(R)) f1 | a! f2, f* . z )
其中 (f1, (f2, f*)) = F = (f1, f2, ..., fn) ，並且 (入 f . R(R)) f1 是一則匿名函數代入參數而生效，計算方式是 R(R)[f1/f] 、即把函數主體 R(R) 中存在的 f 替換為 f1 。在 R(R) 中的 match 定義為
match(b) <= b! r . stop
又取協調程序 C 為
C(b, c) <= rec z . b(r1, (r2, r*)) . ( if r1 = empty then stop
else
if forall r ＜ R . r1 ＞= r then fire(r1)
| b! r2, r* . z )
其中， r1 > r 是一條規則對另一條規則的大於關係，定義為 LHS(r1) ＜ LHS(r) 則 r1 > r ，並且 fire(LHS -> RHS) <= c! RHS . stop 。
又取行動程序 A 為
A(c, d) <= rec z . c(rhs1, (rhs2, rhs*)) . d! rhs1 . c! rhs2, rhs* . z
於是，推論引擎取為
INF(a) <= rec z . a(F, R) . (M(a, b) | C(b, c) | A(c, d) | d(F') . a! (F+F'), R . z)
嗯？有點錯誤，管它的，只是個思考過程。
