Здравствуйте, Курилка, Вы писали:
К>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?
Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>А, сорри, недопонял смысла написаного, дак а что насчёт параморфизма?
L>Нету его
Дак, то что нету это ясно.
Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки.
Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?
L>Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.
Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)?
Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Вот и вопрос — имеет ли смысл за базис чарити брать? К>>Всёж подход Тёрнера мне кажется более вменяемым, но можно транслировать его в код на расширенном чарити... К>>Интерпретатор правда там на Сях К>>Имхо за базис Хаскель брать стоит его задницы мне более симпатичны
L>В смысле ты собираешься сделать такой язык? Отписывайся тогда плз...
Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений )
А то фп-фп, а толку...
Хочется хоть чем-то помочь Родине
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Ещё мысль-вопрос в сторону: наличие НФ для терминируемой функции в итоге даёт возможность точно определить время выполнения функции, исходя из известного времени выполнения неких "примитивных" блоков (базиса языка). Я правильно всё понимаю?
L>Нет, мне кажется. То что у выражения есть НФ не говорит о том, как она достигается. Ведь reduction sequence нам заранее не известен.
Но в языке с ограниченным набором паттернов рекурсии и отделённой кодатой такая оценка возможна, нес па? Выгоды от Тьюринг-неполноты должны же быть?
Здравствуйте, Курилка, Вы писали:
К>Дак, то что нету это ясно. К>Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки. К>Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?
Уи. Только, возможно, я просто чего то недоглядел в Charity.
Здравствуйте, Курилка, Вы писали:
К>Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений ) К>А то фп-фп, а толку... К>Хочется хоть чем-то помочь Родине
Никакого смайла, просто если ты будешь рисовать, то пиши, что получается интересного в процессе — это всё, что я хотел сказать.
Мне будет очень интересно это почитать, пообсуждать.
Здравствуйте, Курилка, Вы писали:
К>Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)? К>Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.
Я не про порядок говорил, а про последовательность — она сильно зависит от данных и то, что в данном случае мы можем быть уверены в терминируемости никак не поможет нам в анализе сложности.
А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.
Здравствуйте, deniok, Вы писали:
D>Но в языке с ограниченным набором паттернов рекурсии и отделённой кодатой такая оценка возможна, нес па? Выгоды от Тьюринг-неполноты должны же быть?
Возможно, я просто не вижу, как её сделать. И потом я говорил не про паттерны рекурсии (типа ката-, ана-) — не про Charity, а про total language вообще — у Тёрнера это, например, структурная декомпозиция.
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Дак, то что нету это ясно. К>>Смотри, по Гёделю формальные алг. системы расширяются за счёт постулатов, выходящих за их рамки. К>>Получается что параморфизм есть пример подобного "выхода за рамки". Не се па?
L>Уи. Только, возможно, я просто чего то недоглядел в Charity.
L>Вот, кстати, нашёл книжку — буду читать L>Categorical programming with inductive and coinductive types
L>Вот тут нашёл: http://www.cs.ut.ee/~varmo/papers/ L>Там ещё до кучи.
У, вкусно
Ещёб время на всё.
Кстати там же внутри система Мартина-Лёфа, помнится nponeccop давал ссылку на Programming in Martin-Lof’s Type Theory — An Introduction, правда тогда я ещё не догнал этого, а Тёрнер её приводит, так что думаю имеет смысл и туда глянуть. Кстати он же делает компилятор, правда ничего не слышно последнюю пару месяцев. Правда на перле и что-то он с комбинаторами мутил (а в комбинаторной логике я слабоват)
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Ну, скажем так, не исключаю такой возможности, про "отписывайся" — это подкол? (без смайла не всегда понятна интонация предложений ) К>>А то фп-фп, а толку... К>>Хочется хоть чем-то помочь Родине
L>Никакого смайла, просто если ты будешь рисовать, то пиши, что получается интересного в процессе — это всё, что я хотел сказать. L>Мне будет очень интересно это почитать, пообсуждать.
Ну слово "отписываться" многозначное, я не то значение выбрал, блин, думал от топика отписываться, чтоб время появилось
Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь
Здравствуйте, Курилка, Вы писали:
К>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь
В московскую я запостил, deniok — стукнешься в питерской, пожалуйста?
Здравствуйте, lomeo, Вы писали:
L>Здравствуйте, Курилка, Вы писали:
К>>Ммм, а если задать "порядок редукции" (или как там ленивость обзывается правильно)? К>>Насколько я понимаю порядок тоже является морфизмом, правда параллели я с ходу боюсь проводить.
L>Я не про порядок говорил, а про последовательность — она сильно зависит от данных и то, что в данном случае мы можем быть уверены в терминируемости никак не поможет нам в анализе сложности.
Тогда можешь пояснить, что тут под последовательностью понимается?
L>А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.
Извини меня, но "как" по-моему не может не влиять на скорость (если ты в Питер через Владивосток поедешь, то есть подозрение, что это будет дольше чем напрямую, правда влияет ещё и механизм перемещения). Нам не нужна НФ. Считаем, что компилятор уже её сгенерил (пофигу каким образом). Речь о том, что передавая параметры мы в интерпретаторе мы получаем некую искомую НФ, в простейшем случае число (e.g. для вычисления факториала), хотя можно его в нумералах Чёрча изображать, тока нафиг?
Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.
Здравствуйте, deniok, Вы писали:
D>Здравствуйте, lomeo, Вы писали:
L>>Вот, кстати, нашёл книжку — буду читать L>>Categorical programming with inductive and coinductive types
D>Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.
Коль ты знаешь его труды, то у него всё в греческих буквочках, практических вариантов нема?
Здравствуйте, Курилка, Вы писали:
К>Кстати там же внутри система Мартина-Лёфа, помнится nponeccop давал ссылку на Programming in Martin-Lof’s Type Theory — An Introduction, правда тогда я ещё не догнал этого, а Тёрнер её приводит, так что думаю имеет смысл и туда глянуть. Кстати он же делает компилятор, правда ничего не слышно последнюю пару месяцев. Правда на перле и что-то он с комбинаторами мутил (а в комбинаторной логике я слабоват)
Много слышал, не читал о Мартин-Лёф ТТ, надо наконец, воспольнить этот пробел. В ТТ разбирается palm_mute, надо его спросить.
Насчёт nponeccop-овского NH0 — то, насколько я понял он транслирует в комбинаторны (какие именно у него рассказыватся). Базис у него, неполный (K не напишешь), но он говорит, что это и не нужно в практических задачах. Смысл, насколько я понял в оптимизации типа суперкомпиляции, но я не уверен.
Здравствуйте, deniok, Вы писали:
D>Это ж диссертация Varmo Vene, известный текст. Он в Тарту заведующий кафедрой. Мы в своё время долго мучались над языком его презентации, оказавшимся эстонским.
А точно! У меня, кстати, такое ощущение было, что я этот текст уже листал. Но не читал, точно
Здравствуйте, Курилка, Вы писали:
К>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь
Здравствуйте, Курилка, Вы писали:
К>Здравствуйте, Курилка, Вы писали:
К>>Думаю имеет смысл инициативную группу собрать, наверное на хугах в феврале стоит рассмотреть этот вопрос. Коллективный разум он помощнее будет, параллелизация понимаешь
К>В московскую я запостил, deniok — стукнешься в питерской, пожалуйста?
Да, только надо сформулировать
Здравствуйте, Курилка, Вы писали:
К>Тогда можешь пояснить, что тут под последовательностью понимается?
Исполнение программы — сначала эту редукцию выполняем, потом эту и так до НФ...
L>>А порядок сам по себе здесь не особо важен — в любом случае НФ будет достигнута. Вопрос в том, как.
К>Извини меня, но "как" по-моему не может не влиять на скорость (если ты в Питер через Владивосток поедешь, то есть подозрение, что это будет дольше чем напрямую, правда влияет ещё и механизм перемещения). Нам не нужна НФ. Считаем, что компилятор уже её сгенерил (пофигу каким образом).
НФ не генерится компилятором. НФ — это то, что мы получаем в результате исполнения программы. И, да, "как" влияет на скорость — я о том и говорил, погляди на выделенное в моем сообщении.
К>Речь о том, что передавая параметры мы в интерпретаторе мы получаем некую искомую НФ, в простейшем случае число (e.g. для вычисления факториала), хотя можно его в нумералах Чёрча изображать, тока нафиг?
Попробую пояснить свою мысль. Значит, мы доходим до НФ в результате исполнения программы. От выбора порядка редукции, разумеется, зависит то, какой будет последовательность этих редукций (исполнение программы). Но сам по себе порядок не важен — просто, зная его, мы знаем, что будет редуцировано на следующем шаге при конкретных данных. Так вот, моя мысль была в том, что автоматический анализ того, какая будет последовательность — сложен. Т.е. "возможность возможность точно определить время выполнения функции" может у нас и есть, только она уж очень теоретическая IMHO.
Но моё "нет" там слишком категорическое. Я погорячился. Надо подумать.
