История изменений
Исправление AndreyKl, (текущая версия) :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формулу f и список переменных xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) наборов переменных truth выражение formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных. formulaDenote вычисляет формулу f на наборе переменных truth.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
кто сказал, что она правильная?
думаю, очевидно
Кстати 
monk, возвращаясь к дискуссии(Зависимые типы, жидкие типы. Что лучше? (комментарий)): а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)
Исправление AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формулу f и список переменных xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) наборов переменных truth выражение formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных. formulaDenote вычисляет формулу f на наборе переменных truth.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
кто сказал, что она правильная?
думаю, очевидно
Кстати monk, возвращаясь к дискуссии: а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)
Исправление AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формул f и список xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) наборов переменных truth выражение formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных. formulaDenote вычисляет формулу f на наборе переменных truth.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
кто сказал, что она правильная?
думаю, очевидно
Кстати monk, возвращаясь к дискуссии: а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)
Исправление AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формул f и список xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) наборов переменных truth выражение formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
кто сказал, что она правильная?
думаю, очевидно
Кстати monk, возвращаясь к дискуссии: а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)
Исправление AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формул f и список xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) переменных truth formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
кто сказал, что она правильная?
думаю, очевидно
Кстати monk, возвращаясь к дискуссии: а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)
Исправление AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формул f и список xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) переменных truth formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.
Кстати
monk, возвращаясь к дискуссии: а вот такое утверждение на «жидких типах» напишется? (я думаю вряд ли)Исходная версия AndreyKl, :
Порождение такой правильной типизации эквивалентно порождению правильного алгоритма,
гм, ну нет
Вот пример. Скажем, задача, написать SMT-solver (https://ru.wikipedia.org/wiki/Задача_выполнимости_формул_в_теориях).
Если говорить кратко, есть список булевских переменных (пусть для простоты [a,b,c]). Ну и есть формула, ну пусть a || (b && c). Пусть нужно определить, есть ли такой набор значений для переменных a, b и c, на котором формула приобретает истиное значение. Или же для всех наборов формула ложна.
В таком случае тип для нашей функции solve принимающий на вход формул f и список xs будет какой-то такой (на Coq).
Definition solve (xs : list bool) (f : formula) : {truth | formulaDenote truth f} + {forall truth, ~~formulaDenote truth f}
Здесь
+ это тип суммы, т.е. логическое или. {truth | formulaDenote truth f} - читается как «Существует переменная truth такая что formulaDenote truth f - истина». {forall truth, ~~formulaDenote truth f} - читается как «Для всех (возможных) переменных truth formulaDenote truth f - ложь» (~~ - отрицание). truth здесь список переменных.Т.е. по русски «либо существует такой набор переменных
truth на котором формула f вычисляется в истину, либо для всех наборов переменных формула f возвращает ложь.»Ну и да, т.к. кок - язык тотальный, то компилятор гарантирует что функция вернёт именно значение этого типа. Т.е. одно из двух.
Но всё таки написать тип - дело ну может 10 минут в данном случае. Алгоритм написать - это уже не так просто.