一大早醒来就人间清醒的发现，mltt里定义的Π，是收缩的。在组合子里这非常直观：

GαβM, αN ⊢ βN(MN)

而实际上这个规则的不收缩版本看上去更直观，它是

GααβM, αN, αN ⊢ βN(MN)

不需要懂什么类型论也能够看出左右守恒了，整个公式仅仅是dual cut，干掉了类型α。

实际上这一点是非常明显的。当G用Ξ组合子写出来时，形式是：

GαβM ≡ Ξα(SβM)

出现S就会出现W，就会导致收缩。

我们来考虑一下前面说的禁止收缩版本的Π/G定义是什么含义。它实际上意味着所有ground类型，都需要标注副本数量。使用一次减少一次。在仿射逻辑下，丢弃没用完的是允许的，使用不存在的不可以。

换句话说，如果有这样的资源限制，马丁洛夫类型论可以扔掉宇宙，因为cut-elim + contraction free意味着，在结构证明论里，已经没有任何规则让前件和后件的公式数量减少了。也就是说，不可能产生悖论，不论现在不可能，以后也永不可能，这不但包括合流停机的λ，也包括不合流但停机的并发扩展，也包括不停机的情况，对于类型系统而言这意味着在系统有懒估值的前提下，无限递归是可以的。

So interesting，这个比pts里带宇宙更精简，而且语法上做了减法但表达力上做了加法，因为它非常自然的带上了对资源的audit。直觉上它自然到，对于并发程序的博弈语义理解，可以表达为当对手抛出资源时，玩家需要出多少资源才能对抗，就像赌博时的筹码一样。