判决中的离奇合同违反答案

【问题标题】：Bizarre Contract Violation in Judgment判决中的离奇合同违反
【发布时间】：2020-03-25 18:53:34
【问题描述】：

我有一个judgement，合同如下：

(define-judgment-form DynamicLam
  #:mode     (down I I O O)
  #:contract (down Γ e Γ e)

  [----------------"Lambda"
   (down Γ_0 z_0 Γ_0 z_0)]
  ;; rest of the code ...
)

当我运行这个时：

(define empty (term ()))
(redex-match? DynamicLam Γ empty)
(redex-match? DynamicLam e lam1^*)
(redex-match? DynamicLam z lam1^*)
(judgment-holds (down empty lam1^* empty lam1^*))

我回来了：

#t

#t

#t

。 . down：判断输入值与其合约不匹配；（由_表示的未知输出值）合约：（下Γ e Γ e）值：（下空 lam1^* _ _）

但这没有意义，因为我上面明明用redex-match?来测试：

empty 匹配 Γ
lam1^* 匹配 e
此外，lam1^* 匹配 z。

我错过了什么？ #:contract 的含义不仅仅是匹配 Γ e Γ e 吗？

【问题讨论】：

标签： racket contract redex

【解决方案1】：

我通过将#:mode 更改为(down I I I I) 而不是(down I I O O) 解决了这个问题，并更改了

(judgment-holds (down empty lam1^* empty lam1^*))

到

(judgment-holds (down ,empty ,lam1^* ,empty ,lam1^*))

, 更改对我来说很有意义，但我仍然不明白为什么需要输入两个输出，所以如果有人可以编辑这个答案来解释这一点，或者提供评论或其他答案解释那种微妙，那太棒了。

【讨论】：