逻辑程序设计：解决术语约束条件f（X; Y; ​​g（a））= f（g（Y）; Z; X）

Question

由于我的精彩，前几天我无法参加我的编程语言课程汽车甩出我。我对我们的家庭作业的工作，我做的还不错，直到我得到了这个可怕看问题：

"5. Solve the term constraint f(X; Y; g(a)) = f(g(Y); Z; X). Show steps." 

现在，我已经读幻灯片，但我不能做什么，他想说的（他来自中国） ，他做了一件很糟糕的工作来解释事情。

我想知道你们中任何一位友善的人是否能够告诉我如何解决类似这样的问题。解释一下，好像我五岁。

谢谢你的时间。

编辑：我是在讲义错节，我发现这一点：

• 任何期限约束，以下列方式处理

•案例1：它的形式为c1 = c2，其中c1和c2为常数 - 如果c1与c2相同，则放弃丢弃它;另有报告无解解

•案例2：这是形式的X = T1（x是一个变量，T1的术语） - 分配T1为x，则丢弃该约束，并取代所有的x在allterm 由t1的约束ift1在它内部没有x;否则报告没有 溶胶iuton

•情况3：ITIS国税发FORMF（S1，...，SN）= G（T1，...，TN）（F，G： 函数符号，Si和Ti：术语） - 如果fisidentical与g相同，则用约束约束条件取代termconstraint约束条件

s1 = t1和s2 = t2，......，sn = tn;否则：无解决方案

- 重复此过程，直到没有更多约束条件或无解决方案解决方案存在的 报告为止。

这对我来说还不是很清楚，我会继续阅读它，直到它完成。我会回复我认为的解决方案，也许你可以告诉我，如果我的解决方案是正确的。

Answer 1

f(X; Y; g(a)) = f(g(Y); Z; X). 

第一步是要注意到，f/3 = f/3，其是壳体3案例3将成功，如果X =克（Y），Y = Z，和G（A）= X.

然后X=g(Y)可能微不足道的是真的;让我们在两侧更换克（Y）X：

f(g(Y); Y; g(a)) = f(g(Y); Z; g(y)) 

OK，一起运动，让我们统一Y及其Z.我没有看到这种情况。

f(g(Y); Y; g(a)) = f(g(Y); Y; g(Y)) 

运动以来，我们接下来的事情就是g(a) = g(Y)。这成功地统一了Y = a。由此产生的术语是：

f(g(a); a; g(a)) = f(g(a); a; g(a)) 

这看起来很明显。 X = g（a），Y = Z = a。

我不知道这是否正确，但这是我的猜测。