PLF练习formal_subtype_instances_tf_2d：S <: S->S类型存在性证明困惑求助

问题核心 #

在无递归类型的简单类型λ演算（STLC）中，不存在类型S满足S <: S->S。

你的当前方法问题 #

你断言S <: S->Top的思路没问题，但这个命题没法帮你导出矛盾，得换个泛化方向。

正确的证明路径 #

1. 明确子类型规则的核心限制：
   在PLF的STLC子类型系统中，只有箭头类型能子类型化箭头类型，Top只能作为所有类型的超类型，不能成为箭头类型的子类型（没有任何规则允许Top <: T->U）。

2. 泛化断言并结构归纳：
   证明更强的命题：对任意类型T，T <: T->T不成立，对T进行结构归纳：

   • 情况1：T = Top
     假设Top <: Top->Top，但没有任何子类型规则支持这个推导（S-Top是所有类型<:Top，反过来不成立；S-Arrow只适用于箭头类型之间的子类型），矛盾，故该情况不成立。
   • 情况2：T = T1->T2
     假设T1->T2 <: (T1->T2)->(T1->T2)，根据S-Arrow规则，必须满足两个条件：
     a. (T1->T2) <: T1 （箭头子类型的定义域反变）
     b. T2 <: (T1->T2) （箭头子类型的值域协变）
     分析条件a：T1->T2是箭头类型，T1要么是Top要么是箭头类型。
     • 若T1 = Top：T1->T2 <: Top是成立的（S-Top），但回到条件b：T2 <: Top->T2。此时T2要么是Top（Top <: Top->Top不成立），要么是箭头类型T2a->T2b，此时T2a->T2b <: Top->T2需要满足Top <: T2a（成立）和T2 <: T2b，会陷入无限循环——但我们的STLC没有递归类型，所有类型都是有限大小的，不可能存在这种无限嵌套结构，矛盾。
     • 若T1是箭头类型：根据归纳假设，T1 <: T1->T1不成立，但这里T1->T2 <: T1，而T1作为箭头类型，要让箭头类型成为它的子类型，根据S-Arrow规则会要求无限嵌套的类型结构，同样与无递归类型的前提矛盾。

3. 矛盾导出：
   两种情况都导出矛盾，故原命题成立——不存在这样的类型S。

内容的提问来源于stack exchange，提问作者L--