Моя кафедра прям так и называлась "Компьютерных наук и экспериментальной математики". Помимо доказуемости или вычислимости есть некий принципиальный нестрогий предел сложности при переходи через который индивид за индивидом теряют способность осознать доказуемые казалось бы вещи. И единственным выходом становится эмпирический подход. Мало того есть мнение, что математический эмпиризм можно спроецировать на все прочие , см. A new kind of science Вольфрама

Я правда не понимаю что такое экспериментальная математика и какие эксперименты они ставят

У меня есть встречный вопрос, и после ответа на него я смогу привести пример. CS - это математика или нет? В частности, вычислимость. (Я считаю да, т.к. теоремы и строгие доказательства)

Я не вполне твердо знаю предмет CS, но вычислимость & Со - самая что ни на есть математика

И это было сделано построением машины Тьюринга, но не формальными методами

Свидетельств, что CS часть математики - много. Хотя найдутся и противоположные точки зрения. Просто потому, что само понятие математики не имеет четкого и единственного определения. Поэтому я предлагаю считать, что там, где есть аксиомы, правила вывода и четкие доказательства - все это математика.

Последнее предложение и есть определение математики. Набор непротиворечивых аксиом + правила вывода.

Доказывается, полагаю, конструированием машины Тьюринга или чем-то похожим. Где эксперимент?

Доказывается, полагаю, конструированием машины Тьюринга или чем-то похожим. Где эксперимент?

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

https://codegolf.stackexchange.com/questions/11880/build-a-working-game-of-tetris-in-conways-game-of-life

Круто. Очень сложно, наверное.

Если понимать задачу вычислимости как задачу поиска Тьюринг-полных систем, то математикой (экспериментальной), внезапно, оказывается и исследование компьютерных игр, таких как Dwarf Fortress, Factorio, Minecraft, и парочки других. Они все Тьюринг-полные (впрочем, про Майнкрафт и Факторио это неудивительно).

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

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

Но, допустим, ты нашел новый способ построить вычислительную систему, эквивалентную машине Тьюринга. И с ее помощью смог показать, например, что P!=NP. Тогда можно говорить, что вокруг вычислимости много задач, и часть из них, вероятно, может быть решена вот такими нестандартными подходами.

CS похож на дискретку

а у дискретной что－то пока нет истовых теоретиков для теории всего

он как-то превращает Bool ~R# Bool в Bool ~R# a в nokinds писали, что в конструкторах хранится a ~ Bool, например, но по факту туда передается сразу Bool ~ Bool при конструировании, как тогда Sub работает

я сделал вывод, что data IntOrBoolTagged a = (a ~ String) => TInt Int | (a ~ Bool) => TBool Bool даже лучше, чем аналогичный gadt data IntOrBoolTagged a where TInt :: Int -> IntOrBoolTagged String TBool :: Bool -> IntOrBoolTagged Bool

потому что более полиморфен, так как работает с поликаиндными (~~) пруфами, хоть нигде явно об этом не написано

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

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

В GHC-8.4.1 это допилили. Теперь и GADT так может. Следующее тайпчекается: data G :: forall k. k -> * where GInt :: G Int GMaybe :: G Maybe

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

теперь там без TypeInType нельзя вроде? или я не те анонсы читал

Не мог обойти стороной. Нужна, программистам, но не вся математика. Я сейчас учусь в универе, и читая чатик теорката или завтипов, ловлю стыд от того, что некоторых вещей не понимаю, хотя в универе проходил.

В GHC-8.4.1 это допилили. Теперь и GADT так может. Следующее тайпчекается: data G :: forall k. k -> * where GInt :: G Int GMaybe :: G Maybe

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

Во всяком случае, больше знать никогда не плохо.

data IntOrBoolTagged (a :: k) where TInt :: Int -> IntOrBoolTagged String TBool :: Bool -> IntOrBoolTagged Bool TMaybe :: IntOrBoolTagged Maybe ну и сейчас же так можно

{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE MultiParamTypeClasses #-} class Source s t where get :: s -> Maybe (t, s) data Parser t a = forall s. Source s t => Parser (s -> [(a, s)]) sat :: (t -> Bool) -> Parser t t sat pred = Parser $ \source -> case get source of Just (t, source') | pred t -> [(t, source')] _ -> [] ---------------------- • No instance for (Source s0 t) arising from a use of ‘Parser’ • In the expression: Parser $ \ source -> case get source of Just (t, source') | pred t -> [...] _ -> [] In an equation for ‘sat’: sat pred = Parser $ \ source -> case get source of Just (t, source') | pred t -> ... _ -> ... | 10 | sat pred = Parser $ \source -> | ^^^^^^^^^^^^^^^^^^^... как-нибудь такое сделать можно? чтобы парсер работал с любым источником токенов?

добрый день, а можете подсказать, я хочу к существующей функции принимающий некоторый тип P разрешить еще принятие другого типа C, внутри преобразовать его к P и вызвать функцию для исходного типа P, пытался сделать как ad-hoc polymorphism, но не получилось

Оно имеет некоторую рекурсивную структуру, и в вызове для P в итоге может появиться вызов для С

Оно имеет некоторую рекурсивную структуру, и в вызове для P в итоге может появиться вызов для С