И никакой попаболи от уебанских попыток технарей в русский язык.
я не гуманятарий
Ты лох
>почему до сих пор нет описательного языка для составления математических абстракций из отдельно взятых детально описанных объектов?
Чем тебя категорно-пучковый язык не устроил?
> почему до сих пор нет описательного языка для составления математических абстракций из отдельно взятых детально описанных объектов?
HoTT.
/тред
А что там непонятно? Let это значит пусть японцы заправляют самолёт и летят уже там смотреть переменные или ещё там чего.
А почему TT, а не просто доказывать теоремы на HOL, Metamath и чем угодно без типо-параши? (серьезно интересуюсь, не тролль)
>HOL
>типо-параши?
>The term "higher-order logic", abbreviated as HOL, is commonly used to mean higher-order simple predicate logic. Here "simple" indicates that the underlying type theory is the theory of simple types, also called the simple theory of types
Ой ну все. Побежал на википедию, увидел знакомы буковки, ручонки затряслись, какой же чудик. Еще бы ты понимал о чем идет речь. Но ничего, я поясню. Например мы можем захотеть отделять высказывания (propositions) от множеств - и бац у нас уже два типа. На самом деле я глубоко с HOL не знаком так что без понятия на сколько там богатая типизация используется, но только иметь типы в языке и пытаться натянуть сову на глобус выстраивая все доказательства только в теории типов с дрочкой вприсядку на швитой изоморфизм - две большие разницы. Или вот еще проще пример untyped lambda calculus - можно сказать та же simple theory of types где есть всего один тип "звездочка".
Из известных компьютер-саентистов - Лесли Лампорт со своим TLA любит публично срать на теорию типов при любом удобном случае.
Правда должен заметить что все эти альтернативные системы все как то мне не заходят совсем. Вот то ли дело петушок дорогой. И может это все не спроста, а все таки швитая сила изоморфизма действует.
> Из известных компьютер-саентистов - Лесли Лампорт со своим TLA любит публично срать на теорию типов при любом удобном случае.
Публично срать все умеют. А вот предложить что-то годное - пикрелейтед. Уже работы де Брауна показали, что без типов никуда. Неявно они все равно используются в любой математике и любым математиком
>Публично срать все умеют. А вот предложить что-то годное - пикрелейтед.
>Лесли Лампорт со своим TLA
Ты реально умственно неполноценный или прикидываешься?
>Уже работы де Брауна показали, что без типов никуда.
Давай рассказывай что они там показали.
>Неявно они все равно используются в любой математике и любым математиком
Типичные трансляции из манямирка, хоть в глаза ссы этим типоблядкам.
это иной уровне абстракции, тут всё понятно, как будто стоишь посреди хвойного леса. ну а ты можешь дальше читать своих дедов.
А зачем индуистам основывать свои учения на еврейской мудрости? У них традиция древнее.
Не все секты и учения апеллируют к древности, хоть и многие.
дурашка, сейчас нельзя поместить человека в дурдом, если он не представляет опасности для общества.
Без моего согласия или согласия проживающих со мной родственников хуй ты куда меня поместишь. Учи законодательство.
если несамостоятельное чмо, то тебе хоть сегодня поместят. Нашелся тут, законодательство ему блеять.