История изменений

Подумай.

f и f' в sup? редуцируются до одинаковой (метатеоретически) нормальной формы, понятное дело.

Давай.

Давай ты не будешь писать _каких-то отдельных_ программ которым _действительно_ не нужны редукции (их не видно, вообще ноль редукций это частный случай для β⋆, то есть transitive closure для бета-редукции), а рассмотришь кучу программ в зависимых типах которым редукция _нужна_ (строго больше нуля редукций, ну как sup?, 5!≡12*10 или a+0≡a).

Открытые термы невозможно редуцировать.

В очередной раз посылаю на the book (которая про LC, множество термов на которых определяется отношение редукции там просто множество термов (big-lambda), никакой закрытости — это отдельный подкласс (big-lambda-zero там, емнип)).

Ну и как бы — «уметь редуцировать открытые термы» (ну как агда) это строго больше «уметь редуцировать закрытые термы» (если это то что ты хочешь называть «бета-редукция»). И уж второе агда тем более умеет делать и делает — нет примеров закрытых термов которые бы не редукцировались у неё в типах (примеров открытых тоже нет, ну да ладно).

Озвучь хоть один пример редукции (как ты её понимаешь) которую нельзя провести в типах — нет такой, иначе это будут нерабочие зависимые типы.

Это как раз дополнительные правила типизации

Это счётное количество «дополнительных правил типизации» называется β-редукция — натурально, все вычисления на термах в наличии при установлении эквивалентности типов. То есть как в омеге наличествуют все «вычисления» на основе операций над типами (при установлении эквивалентности типов, так как типы можно применять к типам), так в зависимых типах есть все обычные вычисления на термах, то есть на основе обычных операций (функций) (тоже при установлении эквивалентности типов, так как типы можно применять к термам — LF).

Это же просто — омега, есть операции на типах и применения типов к типам — надо редуцировать типы при установлении их же эквивалентности, LF — есть применения типов к термам, так что нужно редуцировать ещё и термы обычной бета редукцией, но при установлении эквивалентности именно типов. Omega + LF — и то, и другое. Либо унифицировано как в агде.

Это две разные вещи (до унификации).

При этом

то есть если агда не сумеет «редуцировать» эти термы зависимые типы все равно останутся

тогда это будет как омега без редукций типов (в смысле TAPL), то есть непригодная штука.

ты делаешь вывод о наличии зависимых типов по наличию в системе элементов, которые _не требуются_ для зависимых типов и игнорируя факт отсутствия элементов, которые _требуются_

Редукции как раз требуются. А вот твоё требование на «не constexpr» никак не фигурирует.

Да уже сотню раз приводился подобный пример

Вот каждую твою лямбду я перепишу как template в котором переменная будет параметром шаблона (возьмём для простоты только натуральные числа и size_t в качестве приближения, так как списки в C++ муторно городить), буду утверждать эквивалентность, так что вопрос к чему ты эту лямбду будешь применять — к чему бы ты её не применил, я так же применю шаблон к constexpr терму (и в отличии от лямбда куба тут даже Тьюринг-полнота будет), так что всё сведётся к IO, но в лямбда кубе нет IO, а единственный нормальный способ его добавить это через монаду (как в Agda и Coq), так что что-то изменится только внутри монады, снаружи всё останется как было.

Тут тоже примеров всё ещё нет.

То есть ты серьезно не понимаешь систем лямбда-куба _идейно_, в чем основная фишка каждой из них. То о чем ты говоришь - это фишка омеги, а в зависимых типах того о чем ты говоришь вовсе нету.

Это ты не понимаешь, но я уже привык — fix-в-SystemF-пишется-но-не-типизируется, элементы-у-термов-как-термы-у-типов, ADT-Maybe/List-не-функторы-и-не-монады, что там ещё... Вот теперь ещё отсутствие редукций в зависимых типах :) (в треде была ссылочка — http://oxij.org/note/BrutalDepTypes/, для ленивых).

Ну как же нет? Есть П-типы. До тайпчека включительно. Хотя не совсем понимаю что значит фраза «до тайпчека включительно»

Ну так и в C++ есть подобие П-типов (сум нет, как я понимаю). Фраза значит, что у нас нет «рантайма» — чекнули теоремку (нужен только тайпчек) и разошлись, запускать нечего, либо есть чего в монаде, но нас это не касается (как и нашей системы типов).

такие дела

Ну и достаточно мило, чего :)

Подумай.

f и f' в sup? редуцируются до одинаковой (метатеоретически) нормальной формы, понятное дело.

Давай.

Давай ты не будешь писать _каких-то отдельных_ программ которым _действительно_ не нужны редукции (их не видно, вообще ноль редукций это частный случай для β⋆, то есть transitive closure для бета-редукции), а рассмотришь кучу программ в зависимых типах которым редукция _нужна_ (строго больше нуля редукций, ну как sup?, 5!≡12*10 или a+0≡a).

Открытые термы невозможно редуцировать.

В очередной раз посылаю на the book (которая про LC, множество термов на которых определяется отношение редукции там просто множество термов (big-lambda), никакой закрытости — это отдельный подкласс (big-lambda-zero там, емнип)).

Ну и как бы — «уметь редуцировать открытые термы» (ну как агда) это строго больше «уметь редуцировать закрытые термы» (если это то что ты хочешь называть «бета-редукция»). И уж второе агда тем более умеет делать и делает — нет примеров закрытых термов которые бы не редукцировались у неё в типах (примеров открытых тоже нет, ну да ладно).

Озвучь хоть один пример редукции (как ты её понимаешь) которую нельзя провести в типах — нет такой, иначе это будут нерабочие зависимые типы.

Это как раз дополнительные правила типизации

Это счётное количество «дополнительных правил типизации» называется β-редукция — натурально, все вычисления на термах в наличии при установлении эквивалентности типов. То есть как в омеге наличествуют все «вычисления» на основе операций над типами (при установлении эквивалентности типов, так как типы можно применять к типам), так в зависимых типах есть все обычные вычисления на термах, то есть на основе обычных операций (функций) (тоже при установлении эквивалентности типов, так как типы можно применять к термам — LF).

Это же просто — омега, есть операции на типах и применения типов к типам — надо редуцировать типы при установлении их же эквивалентности, LF — есть применения типов к термам, так что нужно редуцировать ещё и термы обычной бета редукцией, но при установлении эквивалентности именно типов. Omega + LF — и то, и другое. Либо унифицировано как в агде.

Это две разные вещи (до унификации).

При этом

то есть если агда не сумеет «редуцировать» эти термы зависимые типы все равно останутся

тогда это будет как омега без редукций типов (в смысле TAPL), то есть непригодная штука.

ты делаешь вывод о наличии зависимых типов по наличию в системе элементов, которые _не требуются_ для зависимых типов и игнорируя факт отсутствия элементов, которые _требуются_

Редукции как раз требуются. А вот твоё требование на «не constexpr» никак не фигурирует.

Да уже сотню раз приводился подобный пример

Вот каждую твою лямбду я перепишу как template в котором переменная будет параметром шаблона (возьмём для простоты только натуральные числа и size_t в качестве приближения, так как списки в C++ муторно городить), буду утверждать эквивалентность, так что вопрос к чему ты эту лямбду будешь применять — к чему бы ты её не применил, я так же применю шаблон к constexpr терму (и в отличии от лямбда куба тут даже Тьюринг-полнота будет), так что всё сведётся к IO, но в лямбда кубе нет IO, а единственный нормальный способ его добавить это через монаду (как в Agda и Coq), так что что-то изменится только внутри монады, снаружи всё останется как было.

Тут тоже примеров всё ещё нет.

То есть ты серьезно не понимаешь систем лямбда-куба _идейно_, в чем основная фишка каждой из них. То о чем ты говоришь - это фишка омеги, а в зависимых типах того о чем ты говоришь вовсе нету.

Это ты не понимаешь, но я уже привык — fix-в-SystemF-пишется-но-не-типизируется, элементы-у-термов-как-термы-у-типов, ADT-Maybe/List-не-функторы-и-не-монады, что там ещё... Вот теперь ещё отсутствие редукций в зависимых типах :) (в треде была ссылочка — http://oxij.org/note/BrutalDepTypes/, для ленивых).

Ну как же нет? Есть П-типы. До тайпчека включительно. Хотя не совсем понимаю что значит фраза «до тайпчека включительно»

Ну так и в C++ есть подобие П-типов (сум нет, как я понимаю). Фраза значит, что у нас нет рантайма — чекнули теоремку (нужен только тайпчек) и разошлись, запускать нечего, либо есть чего в монаде, но нас это не касается (как и нашей системы типов).

такие дела

Ну и достаточно мило, чего :)

Подумай.

f и f' в sup? редуцируются до одинаковой (метатеоретически) нормальной формы, понятное дело.

Давай.

Давай ты не будешь писать _каких-то отдельных_ программ которым _действительно_ не нужны редукции (их не видно, вообще ноль редукций это частный случай для β⋆, то есть transitive closure для бета-редукции), а рассмотришь кучу программ в зависимых типах которым редукция _нужна_ (строго больше нуля редукций, ну как sup?, 5!≡12*10 или a+0≡a).

Открытые термы невозможно редуцировать.

В очередной раз посылаю на the book (которая про LC, множество термов на которых определяется отношение редукции там просто множество термов (big-lambda), никакой закрытости — это отдельный подкласс (big-lambda-zero там, емнип)).

Ну и как бы — «уметь редуцировать открытые термы» (ну как агда) это строго больше «уметь редуцировать закрытые термы» (если это то что ты хочешь называть «бета-редукция»). И уж второе агда тем более умеет делать и делает — нет примеров закрытых термов которые бы не редукцировались у неё в типах (примеров открытых тоже нет, ну да ладно).

Озвучь хоть один пример редукции (как ты её понимаешь) которую нельзя провести в типах — нет такой, иначе это будут нерабочие зависимые типы.

Это как раз дополнительные правила типизации

Это счётное количество «дополнительных правил типизации» называется β-редукция — натурально, все вычисления на термах в наличии при установлении эквивалентности типов. То есть как в омеге наличествуют все «вычисления» на основе операций над типами (при установлении эквивалентности типов, так как типы можно применять к типам), так в зависимых типах есть все обычные вычисления на термах, то есть на основе обычных операций (функций) (тоже при установлении эквивалентности типов, так как типы можно применять к термам — LF).

Это же просто — омега, есть операции на типах и применения типов к типам — надо редуцировать типы при установлении их же эквивалентности, LF — есть применения типов к термам, так что нужно редуцировать ещё и термы обычной бета редукцией, но при установлении эквивалентности именно типов. Omega + LF — и то, и другое. Либо унифицировано как в агде.

Это две разные вещи (до унификации).

При этом

то есть если агда не сумеет «редуцировать» эти термы зависимые типы все равно останутся

тогда это будет как омега без редукций типов (в смысле TAPL), то есть непригодная штука.

ты делаешь вывод о наличии зависимых типов по наличию в системе элементов, которые _не требуются_ для зависимых типов и игнорируя факт отсутствия элементов, которые _требуются_

Редукции как раз требуются. А вот твоё требование на «не constexpr» никак не фигурирует.

Да уже сотню раз приводился подобный пример

Вот каждую твою лямбду я перепишу как template в котором переменная будет параметром шаблона (возьмём для простоты только целые числа / size_t, так как списки в C++ муторно городить), буду утверждать эквивалентность, так что вопрос к чему ты эту лямбду будешь применять — к чему бы ты её не применил, я так же применю шаблон к constexpr терму (и в отличии от лямбда куба тут даже Тьюринг-полнота будет), так что всё сведётся к IO, но в лямбда кубе нет IO, а единственный нормальный способ его добавить это через монаду (как в Agda и Coq), так что что-то изменится только внутри монады, снаружи всё останется как было.

Тут тоже примеров всё ещё нет.

То есть ты серьезно не понимаешь систем лямбда-куба _идейно_, в чем основная фишка каждой из них. То о чем ты говоришь - это фишка омеги, а в зависимых типах того о чем ты говоришь вовсе нету.

Это ты не понимаешь, но я уже привык — fix-в-SystemF-пишется-но-не-типизируется, элементы-у-термов-как-термы-у-типов, ADT-Maybe/List-не-функторы-и-не-монады, что там ещё... Вот теперь ещё отсутствие редукций в зависимых типах :) (в треде была ссылочка — http://oxij.org/note/BrutalDepTypes/, для ленивых).

Ну как же нет? Есть П-типы. До тайпчека включительно. Хотя не совсем понимаю что значит фраза «до тайпчека включительно»

Ну так и в C++ есть подобие П-типов (сум нет, как я понимаю). Фраза значит, что у нас нет рантайма — чекнули теоремку (нужен только тайпчек) и разошлись, запускать нечего, либо есть чего в монаде, но нас это не касается (как и нашей системы типов).

такие дела

Ну и достаточно мило, чего :)