ML 中的术语并列

Question

我正在尝试翻译以下代码：

(* elim: vname * term * (term * term) list * subst -> subst *)
and elim(x,t,S,s) =
      if occurs x t then raise UNIFY
      else let val xt = lift [(x,t)]
           in solve(map (fn (t1,t2) => (xt t1, xt t2)) S,
                    (x,t) :: (map (fn (y,u) => (y, xt u)) s))
end;

即将从 this repository 转换为另一种语言。我的问题来了，因为我不知道 (xt t1, xt t2) 的语义到底是什么在机器学习中。原则上 xt,t1,t2 是术语，所以我想 xt t1 应该是某种串联（尽管没有定义串联）。

这个代码在 ML 中是什么意思？

为了完整起见，这里是其余相关定义：

type vname = string * int;
type subst = (vname * term) list;
datatype term = V of vname | T of string * term list;

(* lift: subst -> term -> term *)
(* indom: vname -> subst -> bool *)
(* solve: (term * term)list * subst -> subst *)

Answer 1

并列是功能应用。
(a,b) 是一对。

从lift的类型可以看出，lift [(x,t)]——也就是xt——是一个函数term -> term。

因此，(xt t1, xt t2) 是一对 term * term，其第一个元素是将 xt 应用于 t1 的结果，其第二个元素是 xt 应用于 t2.

ML 中的术语并列

Juxtaposition of terms in ML

functional-programming

ml