0

教程 1 第 8 课 ( mu-defined )

我的尝试是替换现有规则：“rule mu X . E => E[(mu X . E) / X]”

规则：

    rule mu X:KVar . E:Exp
    => let X =
    (lambda $x . (( lambda X . E) (lambda $y . ($x $x $y))))
    (lambda $x . (( lambda X . E) (lambda $y . ($x $x $y))))    [macro]"

不幸的是，它不会编译。我究竟做错了什么 ？这个解决方案正确吗？

教程 1 第 8 课 (SK-combinators )

他们在练习的自述文件中有这一部分：

“例如，lambda x . if x then y else z不能按原样转换为组合子，但如果我们假设一个内置的条件函数常量，比如cond，然后对其脱糖if_then_else_，则可以。然后这个表达式变成 lambda x . (((cond x) y) z)，我们知道如何转换。”

我的斗争是与'说' cond，并if_then_else_对其进行脱糖。'

我该怎么做这部分？任何帮助，将不胜感激。

教程 2 第 4 课（纯句法）

他们在练习的自述文件中有这一部分：

'提示：进行顺序组合strict(1)or seqstrict，并让语句减少到{}而不是.; 并且不要忘记创建 {}一个KResult（您可能需要一个新的句法类别，它只包含{}并包含在 中KResult）。

我的斗争是与部分： ' 和有陈述减少到{}而不是.; 并且不要忘记创建 {}一个KResult（您可能需要一个新的句法类别，它只包含{}并包含在 中KResult）'

我该怎么做呢 ？有什么提示吗？

教程 2 第 4 课（未初始化变量）

我创建了以下模块：

module UNDEFINED

    rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->"##") </state>
    requires notBool (X in keys(Rho))

endmodule

但这会用“##”初始化变量。如何用“未定义”初始化变量？有什么提示吗？

教程 3 第 1 课 (callCC)

对于这个练习，我创建了一个与 callcc 非常相似的代码：

    syntax Exp ::= "callCC" Exp  [strict]
    syntax Val ::= cc(K)
    rule <k> (callCC V:Val => V cc(K)) ~> _ </k>
    rule <k> cc(K) V ~> _ =>  V ~> _ </k>

由于某种原因，它不会编译。我究竟做错了什么 ？这个解决方案正确吗？

4

0 回答 0