Identity Inclusion in Relational Type Theory

13:47
 
シェア
 

Manage episode 282601615 series 2823367
著作 Aaron Stump の情報はPlayer FM及びコミュニティによって発見されました。著作権は出版社によって所持されます。そして、番組のオーディオは、その出版社のサーバから直接にストリーミングされます。Player FMで購読ボタンをタップし、更新できて、または他のポッドキャストアプリにフィードのURLを貼り付けます。

Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), RelTT instead has a refinement of this called Identity Inclusion. Instead of saying that the interpretation of every closed type is the identity relation (Identity Extension), the Identity Inclusion lemma identifies certain types whose relational meaning is included in the identity relation, and certain types which include the identity relation. So there are two subset relations, going in opposite directions. The two classes of types are first, the ones where all quantifiers occur only positively, and second, where they occur only negatively. Using Identity Inclusion, we can derive transitivity for forall-positive types, which is needed to derive induction following the natural generalization of the scheme in Wadler's paper (last episode).

122 つのエピソード