Сглаженная форма в WAM

Nov 12 2020

WAM: Tutorial Reconstruction гласит, что запрос p (Z, h (Z, W), f (W)) должен быть сглажен, используя следующие принципы:

При этом уплощенная форма запроса:

X3=h(X2, X5), X4=f(X5), X1=p(X2, X3, X4);

Я заблудился с определением внешней переменной, учтите следующее:

p(Z, h(Y, a(K, C), b(W)), f(W)).

Y - внешняя переменная? Какой должна быть для этого приплюснутая форма? Насколько я понимаю, это будет конструкция:

X1 = p(X2, X3, X4)
X2 = Z
X3 = h(X5, X6, X7)
X4 = f(X8)
X5 = Y
X6 = a(X7, X8)
X7 = K
X8 = C
X9 = b(X5)

Но я не уверен, начиная с X4 я запутался, нужно ли мне сначала назначить внутренние значения h?

Ответы

3 IsabelleNewbie Nov 13 2020 at 08:48

У вас неправильный порядок: вы строите термины до того, как построите их аргументы. В тексте говорится, что нужно строить аргументы, прежде чем строить внешние термины. Например, вы должны построить, a(K, C)прежде чем сможете строить h(..., a(K, C), ...), и вы должны построить это, прежде чем сможете строить p(..., h(..., a(K, C), ...), ...). Вот один законный приказ:

X7 = K
X8 = C
X6 = a(X7, X8)
X5 = Y
X9 = b(X5)
X2 = Z
X3 = h(X5, X6, X7)
X4 = f(X8)
X1 = p(X2, X3, X4)