4 类型表达式等价

如何解释类型表达式相同？

• 主要是考虑到这种情况：在一些语言中存在 typedef 这样的别名功能，比如 typedef UINT unsigned，UINT 的出现作为新的类型或者作为别名，在没有其他约束的情况下可能出现二义性。

• 结构等价、名字等价

结构等价

• 无类型名（别名）时，要求两个类型表达式完全相同
• 有类型名时，用类型名所定义的类型表达式代换别名之后的表达式完全相同（要求别名定义是无环的）
• 结构等价测试（无类型名、环时）

bool sequiv(s, t) {
    if (s和t是相同的基本类型) return true;
    else if (s == array(s1, s2) && t == array(t1, t2)) 
        return sequiv(s1, t1) && sequiv(s2, t2); // 递归检查
    else if (s == s1 × s2 && t == t1 × t2) 
        return sequiv(s1, t1) && sequiv(s2, t2);
    else if (s == pointer(s1) && t == pointer(t1)) 
        return sequiv(s1, t1);
    else if (s == s1 → s2 && t == t1 → t2) 
        return sequiv(s1, t1) && sequiv(s2, t2);
    else return false;
}

名字等价

• 把每个类型名都看成一个需要区别的类型
• 两种类型名字等价 $\Leftrightarrow$ 不做任何名字代换就结构等价

记录类型

记录类型可看成其各个域类型的笛卡尔积类型

记录和积之间的主要区别是：记录的域有名字

typedef struct {
    int address;
    char lexeme[15];
} row;

类型表达式为 record ( address : int, lexeme : array (15, char) )

新增定型规则

$\displaystyle (Type\ Record)\quad\quad\frac{\Gamma\vdash T_1,...,\Gamma\vdash T_n}{\Gamma\vdash record(l_1:T_1,...,l_n:T_n)}\quad l_i\text{ varies}$

变量（$M_i$）记录类型：

$\displaystyle (Val\ Record)\quad\quad\frac{\Gamma\vdash M_1:T_1,...,\Gamma\vdash M_n:T_n}{\Gamma\vdash record(l_1=M_1,...,l_n=M_n):record(l_1:T_1,...,l_n:T_n)}\quad l_i\text{ varies}$

变量成员选择：

$\displaystyle (Val\ Record\ Select)\quad\quad\frac{\Gamma\vdash M:record(l_1:T_1,...,l_n:T_n)}{\Gamma\vdash M.l_j:T_j\quad(1\le j\le n)}\quad l_i\text{ varies}$

类型表示中的环

引入环的话，递归定义的类型名（比如链表、树）可以替换掉

C 语言对除记录（结构体）、共用体以外的所有类型 使用结构等价，而对记录类型用的是名字等价，以避免类型图中的环（上面右图）。

本文阅读量