英文:
PLF: [S <: S->S] Subtyping Example Hint
问题
在编程语言基础课程中，有一个名为 formal_subtype_instances_tf_2d 的练习，要求证明是否存在一种类型 S，使得 S <: S->S 成立。该问题包含一个提示，建议断言该陈述的一般性，并且证明应该按照类型的归纳进行。关于问题的具体细节以及简单类型 λ 演算的实现细节，可以在这里找到：https://softwarefoundations.cis.upenn.edu/plf-current/Sub.html#lab372
我认为不存在这样的类型，因为我认为这个 STLC 实现不允许递归类型。我已成功断言 S <: S->Top。在类型 S 上进行归纳时，我陷入了 S = S1->S2 的情况，一直在努力发展出一个矛盾。这是否是正确的方法，还是我需要不同的断言？
英文:
In Programming Language Foundations, there is an exercise formal_subtype_instances_tf_2d, which is asking to prove whether there is a type S such that S <: S->S. The problem contains a hint that a generalization of the statement should be asserted, and the proof should proceed by induction on a type. The full specifics of the problem and of the simply-typed lambda calculus implementation can be found here: https://softwarefoundations.cis.upenn.edu/plf-current/Sub.html#lab372
I believe there is no such type because I don't believe this implementation of STLC allows recursive types. I have successfully asserted S <: S->Top. Proceeding by induction on S, I am stuck on the case where S = S1->S2 and have been struggling to develop a contradiction. Is this the correct approach, or do I need a different assertion?
答案1
得分: 0
解决方案似乎是对整个陈述进行更广泛的概括。
我使用的概括是 forall S T, S <: {T -> S} -> False。通过对 S（带有依赖的 T）进行归纳来证明它。您可以使用 sub_inversion_arrow 在除一种情况外的所有情况下找到矛盾，即当 S = S1->S2 时。
S = S1->S2 的证明是通过对假设进行反演完成的。这会产生三种情况，可以通过以下方法解决：
- 从假设和重写中得出。
- 在新生成的假设中应用
sub_inversion_arrow，然后注意到S2 <: S1->S2（这可以通过开发一个关于子类型关系的引理，当S1->S2 <: T1->T2时，然后通过子类型关系的传递性来完成），然后剩下的就是假设。 - 从假设中得出。
通过在假设中应用这个概括定理，可以得出对练习的证明。
英文:
The solution seems to be to actually make a broader generalization of the entire statement.
forall S T, S <: <{ T -> S }> -> False is the generalization I used. It is proved by induction on S (with dependent T). You can use sub_inversion_arrow to find a contradiction in all but one case, when S = S1->S2.
The S = S1->S2 is proved by inversion on the hypothesis. This creates three cases which can be solved by the following:
- Follows from hypotheses and rewriting.
- Applying
sub_inversion_arrowin one of the newly generated hypotheses, and then noticing thatS2 <: S1->S2(this can be done by developing a lemma about the subtyping relations whenS1->S2 <: T1->T2, and then by transitivity of subtyping), then the rest follows from hypotheses. - Follows from hypotheses.
The proof for the exercise follows by applying this generalization theorem in the hypothesis.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论