403
правки
Изменения
Нет описания правки
Для работы со списками чисел нам понадобятся следующие функции:
* <tex>\operatorname{empty}</tex> {{---}} возвращает пустой список* <tex>\operatorname{cons}</tex> {{---}} принимает первый элемент и оставшийся список, склеивает их* <tex>\operatorname{head}</tex> {{---}} вернуть голову списка* <tex>\operatorname{tail}</tex> {{---}} вернуть хвост списка
Список будем хранить в следующем виде: <tex>\langle len, p_1^{a_1}p_2^{a_2}\ldots p_{len}^{a_{len}} \rangle</tex>. При этом, голова списка будет храниться как показатель степени при <tex>p_{len}</tex>.
<tex>\operatorname{cons} = \lambda h \to \lambda t \to \operatorname{pair}\ (\operatorname{succ}\ (\operatorname{fst}\ t))\ (\operatorname{mult}\ (\operatorname{snd}\ t)\ (\operatorname{power}\ (\operatorname{ithPrime}\ (\operatorname{fst}\ t))\ h))</tex>
<tex>\operatorname{head } = Lam "\lambda list" $ \to \operatorname{getExponent `App` }\ (\operatorname{snd'' `App` Var "}\ list") `App` \ (\operatorname{ithPrime `App` }\ (\operatorname{pred' `App` }\ (\operatorname{fst'' `App` Var "}\ list")))</tex>
<tex>\operatorname{tail } = Lam "\lambda list" $ \to \operatorname{pair' `App` }\ (\operatorname{pred' `App` }\ (\operatorname{fst'' `App` Var "}\ list")) `App` (\operatorname{eliminateMultiplier `App` }\ (\operatorname{snd'' `App` Var "}\ list") `App` \ (\operatorname{ithPrime `App` }\ (\operatorname{pred' `App` }\ (\operatorname{fst'' `App` Var "}\ list" ))) )</tex>
<tex>\operatorname{eliminateMultiplier' } = Lam "\lambda f" $ Lam "\to \lambda n" $ Lam "\to \lambda m" $ \to \operatorname{if'' `App` }\ (\operatorname{isZero' `App` }\ (\operatorname{mod' `App` Var "}\ n" `App` Var "\ m"\)) `App` \ (Var "f" `App` \ (\operatorname{div' `App` Var "}\ n" `App` Var "\ m") `App` Var "\ m") `App` Var "\ n"eliminateMultiplier = fix' `App` eliminateMultiplier'</tex>
<tex>\ignoreoperatorname{getExponent} = \operatorname{fix}\ \beginoperatorname{codegetExponent'}</tex>
