Обратная функция на Агде

[deni_ok]

Как можно конструктивно доказать, что число 4 является полным квадратом некоторого натурального числа? Предъявив такое число n, для которого n * n = 4.

Comments

[thedeemon]

Занятно, но совершенно бесполезно же - чтобы вычислить обратное значение, надо его же предоставить аргументом.

Вопрос: а можно ли сделать таблицу - массив/список, где n-ный элемент будет содержать Image f ∋ n? В ATS я подобное делал, но через хак по сути.

[deni_ok]

А что этот массив будет содержать для ненаселенных Image f ∋ n? Например, для Image square ∋ 5?

[thedeemon]

Тут я плохо сформулировал, имелось в виду скорее Image f ∋ (f n).

[deni_ok]

Ну проще всего воспользоваться квантором существования (то есть зависимой парой, если размышлять на уровне термов):

list-by-hand : List (∃ λ n → Image square ∋ n)
list-by-hand = (4 , im 2) ∷ (1 , im 1) ∷ (0 , im 0) ∷ []
Теперь обобщаем до заказываемой пользователем длины

list-of-squares : ℕ → List (∃ λ n → Image square ∋ n)
list-of-squares = Data.List.map ( λ x → square x , im x) ∘ downFrom
Ну и, абстрагируясь от square, получим

list-of-images : {Y : Set}(f : ℕ → Y) → ℕ → List (∃ λ n → Image f ∋ n)
list-of-images f = Data.List.map ( λ x → f x , im x) ∘ downFrom

[thedeemon]

И еще вопрос: как в Агде с линейными типами?

[deni_ok]

Ничего не слышал. Интересно подумать над тем, как можно было бы реализовать.

[nivanych]

Вроде, были где-то, надо поискать.

[dima_starosud]

Я когда-то искал, даже в Агда-мейл-лист писал - глухо:(
Но вы поищите, может я недосмотрел.

[nivanych]

Агдочковый курс -
http://www.cs.nott.ac.uk/~txa/g53cfr/
Если делать свой курс, то на этот стоит обратить внимание.

[deni_ok]

Да, спасибо, хороший курс и организован разумно. У нас магистры перегружены, я сомневаюсь, что мне дадут слот под это дело. Может для аспирантов спецкурс удастся сделать, но мне ещё надо некоторое время самому пооттачивать кунг-фу.

[nivanych]

А у вас есть более несколько народу, кому это интересно?

[deni_ok]

Несколько, думаю, наберётся, а больше зачем?