「玩具語言的型別推理原則」修訂間的差異

於 2022年11月10日 (四) 23:11 的最新修訂

$A\in {\{Int,Bool,Flo,String\}}$
${\frac {}{n:A}}$
${\frac {{\textbf {let}}~x:A=y\qquad {y:B}\qquad {belongTo(B,A)}}{x:B}}$
${\frac {{\textbf {let}}~A\in *}{belong(A,A)}}$
${\frac {T_{i},S\in {*}\qquad i=0,1,2,...,n\qquad {\forall j\forall k(~(j\neq {k})~\land ~(j,k\in {i})\rightarrow name_{j}\neq name_{k})}\qquad {{\textbf {typedef}}~S={\textbf {struct}}(item_{0}:T_{0},\dots ,item_{n}:T_{n})}\qquad {x:S}}{x:STRUCT(name_{0}:T_{0},...,name_{n}:T_{n})}}$
${\frac {x:STRUCT(name_{0}:T_{0},...,name_{n}:T_{n})\qquad {i=0,1,\dots ,n}}{x.item_{i}:T_{i}}}$
${\frac {S=STRUCT(name_{S_{0}}:T_{S_{0}},...,name_{S_{n}}:T_{S_{n}})\qquad U=STRUCT(name_{U_{0}}:T_{U_{0}},...,name_{U_{m}}:T_{U_{m}})\qquad m,n\in \mathbb {Z} ^{+}\qquad \forall i\in m\rightarrow name_{U_{m}}\in \{name_{S_{j}}\}\qquad n\geq m}{belongTo(S,U)}}$
${\frac {x_{i}:X_{i}\qquad y:Y,i=0,1,\dots ,n}{(\lambda (x_{0},\dots ,x_{n}).y):(X_{0},\dots ,X_{n})\rightarrow Y}}$
${\frac {x_{i}:T_{x_{i}}\qquad n_{i}:T_{n_{i}}\qquad {belongTo(T_{x_{i}},~T_{n_{i}})}\qquad {i=0,1,...,m}\qquad {foo:((T_{n_{0}},\dots ,T_{n_{m}})\rightarrow Y)}}{f(x_{0},\dots ,x_{m}):Y}}$
${\frac {x_{i}:T_{i}\qquad {\textrm {do}}\{x_{0};x_{1};...;x_{n}\}}{({\textrm {do}}\{x_{0};x_{1};...;x_{n}\}):T_{n}}}$

letrec: 如果 foo 的輸入型別 x_i滿足要求，就假設宣告的 foo 型別 (X₀,...,X_n)→Y 屬性存在。再帶入到函數內部，最後檢查 return 的型別是不是 Y。

@@ 行 1： / 行 1： @@
+{{Nav|程式語言、邏輯學}}
 #<math>A\in{\{Int, Bool, Flo, String\}}</math>
 #<math>\frac{}{n : A}</math>
@@ 行 6： / 行 8： @@
 #<math>\frac{x : STRUCT(name_0 : T_0, ..., name_n : T_n)\qquad{i = 0,1,\dots,n}}{x.item_i : T_i}</math>
 #<math>\frac{S = STRUCT(name_{S_0} : T_{S_0}, ..., name_{S_n} : T_{S_n})\qquad U = STRUCT(name_{U_0} : T_{U_0}, ..., name_{U_m} : T_{U_m}) \qquad m, n \in \mathbb{Z}^+ \qquad \forall i \in m\rightarrow name_{U_m} \in \{name_{S_j}\} \qquad n \ge m}{belongTo(S,U)}</math>
-#<math>\frac{x_i : X_i\qquad y : Y, i = 0,1,\dots , n}{(\lambda(x_0, \dots , x_n).y : (X_0, \dots , X_n))\rightarrow Y}</math>
+#<math>\frac{x_i : X_i\qquad y : Y, i = 0,1,\dots , n}{(\lambda(x_0, \dots , x_n).y) : (X_0, \dots , X_n)\rightarrow Y}</math>
 #<math>\frac{x_i : T_{x_i}\qquad n_i : T_{n_i}\qquad{belongTo(T_{x_i},~T_{n_i})}\qquad{i=0,1,...,m}\qquad{foo: ((T_{n_0}, \dots, T_{n_m})\rightarrow Y)}}{f(x_0,\dots, x_m) : Y}</math>
+#<math>\frac{x_i : T_i\qquad\textrm{do}\{x_0; x_1;...; x_n\}}{(\textrm{do}\{x_0; x_1;...; x_n\}): T_n}</math>
+letrec: 如果 foo 的輸入型別 x<sub>i</sub>滿足要求，就假設宣告的 foo 型別 (X<sub>0</sub>,...,X<sub>n</sub>)→Y 屬性存在。再帶入到函數內部，最後檢查 return 的型別是不是 Y。
+[[category:資訊]]