Я новичок в Idris и пытаюсь уловить основные понятия и синтаксис.
Даже если это может показаться бессмысленным, я пытаюсь определить функцию half, которая вдвое уменьшает натуральное число.
Я хочу придумать что-то вроде:
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
но конечно не работает. В частности, я получаю:
ошибка: ожидается: подпись зависимого типа
half : (n : Nat) -> (k : Nat) -> (n = k + k) -> (k : Nat)
Является ли это возможным?
Спасибо.
Вы хотите выразить, что half n есть некоторое Natуральное число k такое, что n = k + k выполняется. Это можно сделать с помощью сигма-типа, то есть зависимой пары число k и доказательство n = k + k (это зависимая пара, поскольку тип второй координаты, n = k + k, зависит от значения первой координаты, k).
Стандартная библиотека Idris определяет DPair для зависимых пар, включая некоторый синтаксический сахар, позволяющий писать
half : (n : Nat) -> (k ** n = k + k)
Однако обратите внимание, что вы не сможете реализовать half (как общую функцию), потому что нет хорошего ответа, например. half 1. Может быть, то, что вы хотите, это
half : (n : Nat) -> (k ** Either (n = k + k) (n = k + k + 1))
?
half: (n : Nat) -> Even n -> Nat с дополнительной информацией о том, что полученное Nat на самом деле является первым Nat, разделенным пополам. В вашем случае является ли функция total (т.е. принимает на вход только даже Nat)? Тот факт, что вы используете Eirther, заставляет меня думать, что это не так, в то время как в первой версии мы должны предоставить half доказательство того, что n четно, что исключает 1, 3 и все остальные нечетные числа. В очередной раз благодарим за помощь.
- person Cristiano Paris; 01.12.2016
n равен либо 2 * k, либо 2 * k + 1. Конечно, первый не может, так как нет k такого, что, например. 1 = 2 * k.
- person Cactus; 01.12.2016
Вы не должны использовать k дважды. половина : (n : Nat) -> (k : Nat) -> (n = k + k) -> Nat правильно, но бесполезно. Я думаю, вам нужно половина: (n: Nat) -> Возможно (k ** n = k + k)
