способом: reverse1([a1, a2, ..., ai, ..., an]) = [an, a_(n-1), ..., ai, ..., a1], то для такого случая можно ли показать, что reverse1 == reverse?
Я так понимаю, тут придется сделать индексированный список и уже потом что-то доказывать. Хотя, надо как-то понять, что две структуры данных отражают одно и то же
Это не является определением на формальном языке. Если его формализовать, то придешь к той же самой "неинтуитивной" рекурсии, но на индексах, дальше применяешь морфизм из индекса в значение и получаешь то же самое определение
А почему это не является определением на формальном языке?
я не настоящий сварщик, но список же задан как Nil | Cons a (List a) (условно), а не как элементы с индексами
Ну можно data Nat = Z | S Nat data Vect (n :: Nat) where VNil :: Vect Z VCons :: a -> Vect n -> Vect (S n)
так у тебя всё равно используется в определении reverse некий синтаксис [a, b, c], который из твоего определения списка не следует и как с ним работать — неочевидно
теоретически можно сопоставить индексы элементам конечного списка. но это ещё надо доказать как лемму
Вот именно. И как их сопоставить — я не знаю
основной способ доказательства это по индукции индукции соотвествует рекурсия если у тебя нерекурсивное определение, то индукцию будет применить сложно придется сводить такое определение к рекурсии как-то, типа отрывать по одному и смещать индексы
Обсуждают сегодня