kframework - K 中的高阶函数？

Question

是否可以在 K 中编写高阶函数？

Map特别是and之类的东西Fold，我遍历结构并将函数应用于每个元素。

例如，如果我有一个列表：

A ~> B ~> C

我想将一个函数映射F到列表的每个元素：

F A ~> F B ~> F C

或者可能会产生折叠：

F A (F B (F C))

where Fis[function, functional]并且是用来评估的，而不是语法上的。

Answer 1

如果您知道要以更高阶的方式使用哪些功能，您可以使用以下方法进行近似：

syntax MapFunction ::= "foo"
syntax KItem ::= MapFunction "(" KItem ")" [function]

rule foo(...) => ...

syntax List ::= map(List, MapFunction) [function]
rule map(.List, _) => .List
rule map(ListItem(K) L, F) => ListItem(F(K)) map(L, F)

我认识到这并不理想，因为它并不是真正的高阶函数，您必须明确了解您打算以这种方式使用的每个函数并以不同的方式编写它，但如果您只需要快速的东西，这是一个不错的解决方法在语义上的几个地方很脏。

至于您的其他问题，我们希望更普遍地支持高阶函数，但我们还没有。