- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
Короче, размышлял я как-то на тему того, как надо делать правильный
теорем прувер, а не питушню всякую заедушную. Вот взять тот же Metamath -
там какие-то непонятные distinct правила для хуиты, что надо какие-то там
disjoint переменные, вот тут https://groups.google.com/g/metamath/c/M2dUfFATxD8
про это подробнее сказано.
Есть вот еще Metamath zero https://github.com/digama0/mm0 и это вот кажется ближе
к тому, что мне нравится.
Например вот https://github.com/digama0/mm0/blob/master/examples/assembler.mm1
тут есть какая-то теорема про ELF хедер. Это вот определение ELF идентификатора
local def ELF_IDENT_s: string =
$ ,0x7f ': ,"E" ': ,"L" ': ,"F" ':
_x02 ': _x01 ': _x01 ': _x00 ': _x00x8 $;
и там еще какой-то такой хуйней описывается то, где там точка входа записана в заголовке,
еще separation logic есть какая-то.
Но вот если почитать спецификацию для этого mm0 языка
https://github.com/digama0/mm0/blob/master/mm0.md :
pure means that this sort does not have any term formers. It is an uninterpreted domain which may have
variables but has no constant symbols, binary operators, or anything else targeting this sort. If a sort has
this modifier, it is illegal to declare a term with this sort as the target.
strict is the "opposite" of pure: it says that the sort does not have any variable binding operators. It is illegal
to have a bound variable or dummy variable of this sort, and it cannot appear as a dependency in another
variable. For example, if x: set and ph: wff x then set must not be declared strict. (pure and strict are not
mutually exclusive, although a sort with both properties is not very useful.)
provable means that the sort is a thing that can be "proven". All formulas appearing in axioms and theorems
(between $) must have a provable sort.
free means that definitions and theorems are not allowed to use dummy variables with this sort.
то кажется мне, что слишком это сложно. Надо проще это всё сделать, по принципу какой-нибудь
хрени типа SKI кобенационного исчисления. Т.е. допустим аксиома для модус поненса
AXIOM
%A
P P $IMP %A %B
_
%B
т.е. если мы матчим некую хуйню "%A" и некую хуйню "P P $IMP %A %B" где %A и %B это некая
срань, которая может быть "что-то" "P чтото чтото" или там "P чтото P чтото чтото" и т.д.
ну короче P означает что там две какие-то хуйни, вот как в той хрени https://govnokod.ru/27420
то можем дополнительно синтезировать высказывание "%B"
А теоремы это negj композиции из аксиом и других теорем. Типы можно прикручивать через какую-то хуйню
типа если арифметику Пеано описывать, тип можно так что-то нахуевертить аксиому, ну типа
Определение что ZERO это натуральное число.
AXIOM
_
P NAT ZERO
Что если инкрементнуть натуральное, будет тоже натуральное (S это функция следования)
AXIOM
P S %A
P NAT %A
_
P NAT P S %A
В общем надо бы подумать, как там запилить максимально простой и эффективно расширяемый язык для
доказывания всякой хуйни.
Смотрел Coq - какая-то ебаная перепитушня со всякими там типами-хуипами и какими-то
блядь рекурсиями. Хер поймешь, как эта вся дрнсня работает. Меня ваши типы не ебут
совершенно, я хочу сам свои типы конструировать, а не полагаться на какую-то невнятную
ебанину.
j123123 05.07.2021 11:21 # +1
bormand 05.07.2021 11:26 # +1
Потому что большинство устраивают собачки в ПХП. К счастью или к сожалению.
1024-- 05.07.2021 18:00 # 0
1. Заказчикам не приходится нанимать докторов наук по кокам и хачкелям, чтобы реализовать задачу, которую может сделать школьник.
2. У технологий повышается "порог вхождения" в мир. Если ещё 40 лет назад можно было скормить ничего не подозревающему человеку assемблер и шишку, то сейчас мало кто захочет изучать что-то менее человечное, чем питон и шишарп. Чем дольше мы ждём, тем меньше интереса будет у людей к пердольной питушне.
Но специалисты понимают, что собачки кусаются, и некоторые концепции были бы полезными. А значит с течением времени в какой-то инструмент вложится очередной майкроугл. Тогда появится одно решение, рассчитанное на нормальных людей.
Не куча сделанной наполовину питушни - как вышло с языками программирования, а один хороший и интуитивно понятный продукт, для которого достаточно степени выпускника средней школы, и на его фоне куча остальной "разрозненной хуиты" для докторов, где у пакетного менеджера нет команды "удалить пакет", а для вывода на консоль надо знать теорию категорий и монады.
Coq 05.07.2021 11:56 # +1
bormand 05.07.2021 11:42 # +1
Нясколько понямаю, в coq хотели дать тебе няпротиворечивую систему, в которой ты ня можешь отстрелить себе ногу. Числа, логические операторы и т.п. там строятся из очень простых вещей. Да, ня поверхности выглядит сложня и страшня, но под капотом там по сути просто лямбды да их типы ^_^
А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор. Конпелятор ня сможет проверить, что твоя няксиоматика ня поехавшая. Тебе придётся как-то самому вручную доказывать, что новая няксиома ничего ня портит.
З.Ы. Да, в coq, нясколько я понямаю, вообще нявозможно добавить реальную няксиому. Твой пруф будет просто импнякацией при условии что эта "няксиома" верна. Сам движок ня верит в её истинность.
j123123 05.07.2021 12:08 # 0
Нет доказательств непротиворечивости coq. Есть столько же оснований доверять непротиворечивости кем-то написанным аксиомам, как и доверять непротиворечивости coq. В самом coq доказать непротиворечивость coq невозможно, потому что вторая теорема Гёделя о неполноте.
Если формальная арифметика S непротиворечива, то в ней невыводима формула, содержательно утверждающая непротиворечивость S.
> А твоя версия с няксиомами -- это как няшная с её UB'ами: някаких подушек безопаснясти, только хардкор.
А как мне помогает coq? Если я в coq описываю некую свою хуйню, например аксиомы из theory of array https://smt2012.loria.fr/paper1.pdf
These axioms state that storing the value v into an array a at index p and subsequently reading a’s value at index q results in the value v if the indices p and q are identical. Otherwise, the write operation does not influence the result of the read operation.
Каким образом coq защитит меня, если я при переписывании этих аксиом где-нибудь ошибусь?
bormand 05.07.2021 12:14 # 0
Т.е. тот же массив ты мог бы построить в виде списка или дерева. И ня освнове этого вывести его свойства. И тогда ты можешь ня бояться, что они записаны няправильно. Ты просто не сможешь их доказать.
Почему в данной работе они пошли в обход системы -- я ня знаю, честно.
guest6 05.07.2021 12:16 # +4
bormand 05.07.2021 12:44 # +1
guest6 05.07.2021 12:52 # +1
bormand 05.07.2021 12:55 # +1
guest6 05.07.2021 12:58 # +2
1024-- 05.07.2021 17:42 # 0
j123123 05.07.2021 12:18 # 0
Для этого тебе надо построить из чего-то список или дерево (или чтобы список или дерево уже было). А никаких списков и деревьев может не быть. И вообще, может лучше я сначала построю theory of array, и потом поверх нее построю списки и деревья.
Как все настоящие программисты знают, единственной полезной структурой данных является массив. Строки, списки, структуры и наборы — это все разновидности массивов и их можно рассматривать как массивы без усложнения вашего языка программирования.
bormand 05.07.2021 12:20 # 0
j123123 05.07.2021 12:24 # 0
bormand 05.07.2021 12:38 # 0
Но, как мне кажется, когда ты добавляешь в свою систему какую-то новую сущность, выгоднее её выразить в терминах существующих, а ня ебашить няксиомы о ней. Меньше рисков получается.
guest6 05.07.2021 12:39 # 0
bormand 05.07.2021 12:41 # 0
j123123 05.07.2021 16:35 # 0
Это, вообще говоря, не важно. Можно сделать аксиоматику для массивов с нуля, и можно параллельно сделать аксиоматику для деревьев с нуля, а потом формально доказать, что массивы вот так можно описать через деревья, и что деревья можно вот так описать через массивы. Т.е. что такие-то рассуждения в теории массивов изоморфны таким-то рассуждениям в теории деревьев, и это все тождественно.
bormand 05.07.2021 17:10 # 0
По сути, на практике ты будешь доказывать что-то в духе изоморфизма конструкций твоего DSL'а и инструкций какого-нибудь arm'а или x86. А посрединке между ними будут всякие теории о массивах, деревьях, лямбдах и т.п. В каком из базисов ты это делаешь -- не так уж важно, их бесконечно много. Лишь бы выбранный базис не позволял доказывать хуйню на ровном месте.
j123123 05.07.2021 20:09 # 0
А судьи кто? Как оценивать сложность? Я вот например не уверен, что теория массивов чем-то сложнее теории деревьев.
bormand 05.07.2021 20:10 # 0
j123123 05.07.2021 20:30 # 0
И что? Любая вычислимая функция выражается через программу на языке брейнфак, но это не значит, что любую вычислимую хрень надо сводить к брейнфаку и в неких брейнфак-аксиомах доказывать. Если ты доказываешь корректность сортировки пузырьком на языке Си, ты будешь на брейнфаке описывать некий Си-интерпретатор который запускается в брейнфаке, а потом доказывать через брейнфак-аксиоматику, что если мы в брейнфак засунем Си-интерпретатор и в Си-интерпретатор скормим такой-то код сортировки на Си, то эта сортировка будет работать как надо?
bormand 05.07.2021 21:04 # 0
Ну не совсем так. Допустим, я построила массивы на брейнфаке (х.з. как это делать, если честно) и доказала несколько теорем о них (те самые утверждения, что ты привёл как аксиомы).
Теперь я могу эти теоремы юзать чтобы доказать что-то более интересное и высокоуровневое. Что сортировка сортирует, к примеру. И ни я ни тайпчекер не будем углубляться в детали реализации этих массивов пока не понадобится какая-то новая хитровыебанная теорема о них.
Или я могу попытаться на основе брейнфака выразить лямбда-исчисление и дальше уже пользоваться им, забыв на время о брейнфаке.
Т.е. базис -- это просто базис.
j123123 06.07.2021 08:39 # 0
Много способов есть. Можешь переписать Coq на брейнфак и в Coq построить массивы.
bormand 05.07.2021 12:17 # 0
JloJle4Ka 05.07.2021 12:18 # 0
bormand 05.07.2021 12:21 # 0
guest6 05.07.2021 12:36 # 0
JloJle4Ka 05.07.2021 12:45 # +1
Логика высказываний, пропозициональная логика или исчисление высказываний, также логика нулевого порядка — это раздел символической логики, изучающий сложные высказывания, образованные из простых, и их взаимоотношения.
Исчисление конструкций — теория типов на основе полиморфного λ-исчисление высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — \lambda P\omega.
Хотя, ладно, понятно почему.
Hijikata 05.07.2021 18:56 # +1
Hijikata 05.07.2021 18:57 # +1
§5.4
j123123 05.07.2021 20:05 # 0
А это доказательство на самом Coq есть? Вот есть всякие примеры, когда из Coq синтезируют некоторые корректные по построению программы, кто-нибудь смог на Coq сгенерить корректный по построению Coq и его потом им же опять так пересобрать? (т.н. раскрутка компилятора)
Hijikata 05.07.2021 20:39 # 0
j123123 05.07.2021 20:52 # +1
Да, это понятно, я о том, чтобы добавить аксиом, чтобы доказать непротиворечивость того Coq, где этих аксиом нет.
Когда некие математики доказывали эту сильную нормализацию для исчисления конструкций, они опирались на какие-то аксиомы, правила вывода. Если эти аксиомы существуют, их можно записать в Coq тоже как некие аксиомы, тут я не вижу противоречия. Или эти аксиомы невыразимы в Coq? Как такое может быть?
Если рассматривать некую формальную систему "X" в которой невыводима непротиворечивость "X" но нам надо доказать ее непротиворечивость, мы создаем некую расширенную формальную систему "X++" в которой доказуема непротиворечивость "X" (но непротиворечивость "X++" уже недоказуема). Похоже что это т.н. метасистемный переход
j123123 05.07.2021 20:59 # 0
хмм...
j123123 09.07.2021 13:52 # 0
типа
j123123 09.07.2021 13:52 # 0
Т.е. что если есть аксиома
то можно синтезировать аксиому
а потом еще и аксиому
и так до бесконечности. Надо чтоб метасистемный переход.
Hijikata 05.07.2021 21:14 # +3
j123123 05.07.2021 21:06 # 0
j123123 05.07.2021 21:12 # 0
bormand 05.07.2021 21:16 # −1
j123123 05.07.2021 21:32 # 0
j123123 05.07.2021 21:38 # 0
bormand 05.07.2021 22:34 # −1
(& (& (& f a) b) c)
Будет лучше видно структуру для паттерн-нятчинга.
bormand 05.07.2021 22:39 # −1
Ну просто у тебя уже есть скобочки, а ты унарный оператор пердолишь.
j123123 05.07.2021 23:13 # 0
bormand 05.07.2021 23:17 # 0
j123123 06.07.2021 06:19 # 0
В общем это все синтаксический сахарок, который можно внешним препроцессором сделать, тащить это в базовый язык незачем.
bormand 05.07.2021 22:50 # 0
j123123 05.07.2021 21:17 # 0
Вот так надо, потому что "not" принимает один аргумент
Desktop 05.07.2021 21:19 # +1
- показалось
bormand 05.07.2021 21:26 # 0
HEu3BECTHblu_nemyx 05.07.2021 21:27 # 0
bormand 05.07.2021 21:52 # 0
Может быть какие-то безусловные (& wff true) и (& wff false) стоит добавить чтобы можно было начать что-то строить?
j123123 05.07.2021 22:15 # 0
А зачем тебе что-то брать? Теоремы ты строить можешь. Например транзитивность http://us.metamath.org/mpeuni/syl.html - если "из a следует b" и "из b следует c" то "из a следует c"
Никакой (& wff true) и (& wff false) не нужен.
Если @a @b @c это wff (well formed formula), мы тривиально доказываем что "& & imp @a @b" и "& & imp @a @c" это тоже wff и так можем эту теорему применить в какой-то другой теореме.
bormand 05.07.2021 22:17 # 0
j123123 05.07.2021 22:18 # 0
j123123 05.07.2021 22:24 # +1
но суть, думаю, ясна
guest6 05.07.2021 22:26 # −1
bormand 05.07.2021 22:52 # 0
j123123 05.07.2021 22:56 # 0
bormand 05.07.2021 23:15 # 0
Может более явный синтаксис сделать, что у аксиом и теорем есть только одно утверждение:
j123123 05.07.2021 23:20 # 0
bormand 05.07.2021 23:22 # 0
Т.е. получается что какие-то элементы логики уже прям в синтаксис просочились. А мы их потом заново сочиняем.
j123123 05.07.2021 23:30 # 0
А как определять это самое "И", если бы в теореме-аксиоме нельзя упомянуть две или более штуки?
Ну т.е.
bormand 05.07.2021 23:34 # 0
forall a b, a -> b -> and a b
Теперь вопрос как импликацию аксиоматизировать...
j123123 05.07.2021 23:42 # 0
bormand 05.07.2021 23:44 # 0
Если верно а, тогда (если верно b, тогда верно and a b).
Или я туплю?
j123123 05.07.2021 23:50 # 0
Вообще это проблема курицы и яйца.
bormand 05.07.2021 23:53 # 0
В петухе ее элегантно решили построением и того и другого через лямбды и типы, но здесь видимо так не прокатит ;(
CHayT 06.07.2021 20:11 # +1
bormand 06.07.2021 20:19 # 0
1024-- 07.07.2021 11:28 # +2
А j123123 какой-то ассемблер сделал или сишку с кучей &мперсандов и переводов строки. Читается как чат малолеток:
- ты как няш :*
- норм ))
- ясн ))
- а ты7
- неоч (((
- бл& (
- вще х&&во
- &здец ))
bormand 07.07.2021 11:30 # 0
Из-за RPN что-то сложнее этой теоремки будет нячитаемо, ну да пофиг. Плюс тут надо как-то задекларировать wff и and перед использованием:
2 constructor and
1 constructor wff
1024-- 07.07.2021 11:41 # 0
А то если гуглить, это либо Росприроднадзор, либо оперативный ответвительный зажим, либо registered practical nurse, либо revenue payroll notification.
Хотя, с другой стороны, может и не надо такое гуглить, а то потом начну писать теоремы и формулы вида E=mc^2 записывать с амперсандами и скобками
bormand 07.07.2021 11:42 # 0
1024-- 07.07.2021 11:44 # 0
bormand 07.07.2021 11:38 # +1
Вообще говоря, в этом и идея. Ядро прувера и должно быть простым и похожим на ассемблер. А дальше поверх него уже можно наворачивать всякий сахарок и тактики без боязни обосраться.
1024-- 07.07.2021 11:59 # 0
j123123 07.07.2021 12:29 # 0
Вот допустим
надо чтоб где-то в определении "+" было описано что оно захавывает из стека два "Nat" и "возвращает" один "Nat". И что "5" вообще нифига не захавывает, и просто является "Nat".
И если есть теорема, что "@x @x +" где @x это "Nat" можно переписать как "@x 2 *", и чтоб такую теорему применить нужным образом, если указать что "@x" это "5 5 +" то тогда питушня заматчится так
А если указать что "@x" это "5" то
Надо какой-то дополнительной питушней указывать, когда надо матчить? В общем, это немного усложняет
bormand 07.07.2021 12:54 # 0
В префиксном формате у тебя есть точно такая же проблема (да и в инфиксном коке она тоже есть).
Допустим, мы хотим применить теорему про a + b = b + a в формуле (1 + 2) + (1 + 2). Здесь три потенциальных матча. Как указать, какой именно я хочу зареврайтить? Т.е. в любом случае надо какой-то способ для явного выбора нужного фрагмента.
j123123 07.07.2021 13:53 # 0
надо матчить не через
а через
Или даже чтоб
И тогда в @z1 задаем
а в @z2 - нихуя.
bormand 07.07.2021 13:58 # 0
bormand 07.07.2021 14:11 # 0
'& & plus @c & & plus @b @a'
Кстати, а как ты это докажешь имея только если '& & plus @a @b' то '& & plus @b @a'?
Воспользуешься дополнительной леммой если '@x = @y' то '& & plus @c @x' = '& & plus @c @y'? Или как-то проще, чтобы эквивалентность не вылезала?
j123123 07.07.2021 22:28 # 0
Ну допустим если использовать прямую польскую запись и отказаться от этих вот "&"
bormand 08.07.2021 00:53 # 0
Имхо, тут можно попробовать доказать лемму конгруэнтности (или как там её правильно зовут): если из @a следует @b, то из plus @x @a следует plus @x @b, а так же из plus @a @y следует @b @y. Имея такие леммы можно будет легко добираться до нужных фрагментов.
Но я пока туплю, как её записать в твоей системе.
bormand 08.07.2021 01:05 # 0
j123123 08.07.2021 10:49 # 0
У тебя ж тут ничего ничему не равно и даже не имплицируется.
Хотя наверное можно попереставлять, потом собрать выражение с импликацией и его применить по такой-то аксиоме. Это думать надо
j123123 08.07.2021 11:05 # 0
j123123 08.07.2021 11:08 # 0
bormand 08.07.2021 14:08 # 0
a+(b+c) = (a+b)+c = (b+a)+c = b+(a+c)
Но тут опять же нужна конгруэнтность плюсика (x=y -> a+x=a+y /\ x+a=y+a), чтобы можно было оперировать над кусками формулы, а не над всей целиком.
В коке она бай дизайн, насколько понимаю. А тебе её придётся доказать или принять.
bormand 08.07.2021 01:09 # 0
j123123 08.07.2021 09:10 # 0
http://us.metamath.org/mpeuni/ax-mp.html
bormand 08.07.2021 01:11 # 0
bormand 08.07.2021 01:17 # 0
CHayT 08.07.2021 01:27 # +1
bormand 08.07.2021 01:30 # +1
j123123 08.07.2021 15:16 # +1
booratihno 08.07.2021 15:17 # +1
j123123 08.07.2021 09:19 # 0
bormand 07.07.2021 14:26 # 0
Это как-то постулируется в твоей аксиоматике? Или есть какой-то пруф? Или это нужно доказать в каждом кейсе перед тем как реврайтить?
j123123 07.07.2021 14:59 # 0
Не, ну это надо просто хуйни не делать. Если есть какая-то хуйня, где можно "перегружать" значение plus, и при такой перегрузке plus уже не складывает, а возводит в степень, и эта хуйня для перегрузки заматчилась в @z1 @z2 (как в том последнем примере) то конечно хуйня будет.
Тут надо конкретику обсуждать, придумывать непосредственно сами аксиомы и правила вывода
bormand 07.07.2021 15:23 # 0
Пока это выглядит как деревья, состоящие из атомов (wff, and и т.п.) и конструкторов пары (&).
Над деревьями мы вводим отношение истинности. Какие-то деревья истинны, а какие-то -- нет.
Но пока у нас нет способа показать, какие из них истинны. Для этого мы вводим аксиомы, которые в простейшем случае могут сказать, что какое-то конкретное дерево истинно.
Но работать над конкретными деревьями скучно, поэтому мы вводим собачки-переменные (ака forall) чтобы составлять более интересные аксиомы, которые гласят "такое дерево истинно для любых поддеревьев @a".
И затем мы вводим ещё более сложные аксиомы, в которых есть набор входных условий: "если все вот эти деревья истинны для поддерева @a, то вот такое дерево тоже истинно для этого @a".
Поправь меня, если я написала хуйню.
З.Ы. Т.е., насколько я понимаю, пока что мы можем применять теоремы только от корня, ко всему дереву целиком. Права на работу с поддеревьями у нас пока нету.
j123123 07.07.2021 15:43 # 0
Тут изначально нет никакой "истинности". Тут речь о выводимости т.е. можем ли мы такую-то штуку сконструировать, пользуясь такими-то аксиомами и/или уже доказанными теоремами. Если можем, то теперь эта штука - еще одна теорема, которой можно пользоваться для доказывания чего-то там.
bormand 07.07.2021 15:44 # 0
j123123 07.07.2021 15:59 # 0
Что-то мне подсказывает, что этот "&" тоже можно обычным термом считать, никакого особого статуса ему можно не давать (хотя может это где-то что-то ломает, но пока это неочевидно). И тогда никаких деревьев тут по-сути нет, просто списки хреней, которые матчатся какой-то хреню и если заматчились то генерируем что-то там.
CHayT 07.07.2021 16:03 # +3
Это же sed (=^ ◡ ^=)
bormand 07.07.2021 16:14 # 0
Да в общем-то его тогда и выкинуть можно, записывая "& & and" как "and". Вроде тоже ничего не сломается.
bormand 07.07.2021 16:24 # 0
wff @a -> wff not @a
wff @a -> wff @b -> wff and @a @b
То хуёвую формулу из них ну никак не слепить, насколько я понимаю. Можно даже попробовать это пруфнуть.
& разве что для каррирования мог бы пригодиться. Типа "& and @a" -- это унарная хуйня, принимающая bool. Другой пользы я пока не вижу.
j123123 07.07.2021 16:25 # 0
которая через какие-то теоремы переписывается по частям
j123123 07.07.2021 16:33 # 0
bormand 07.07.2021 16:34 # 0
В пруверах про такое обычно не парятся... ну да ладно.
У тебя там всё равно end есть. Так что можно как-то так зареврайтить:
add_many end_add_many -> 0
add_many @a -> add @a add_many (в этом правиле @a должно быть wff)
add_many @a @b @c end_add_many ->
add @a add_many @b @c end_add_many ->
add @a add @b add_many @c end_add_many ->
add @a add @b add @c add_many end_add_many ->
add @a add @b add @c 0
CHayT 07.07.2021 16:41 # +1
Не преумняжай сущнясти. Все функции принимают на вход только один аргумент, а с зависимыми типами можно намутить, что при каррированяи тип возвращаемой лямды будет отличаться в зависимости от предыдущих аргументов.
CHayT 07.07.2021 16:46 # +1
bormand 07.07.2021 16:47 # 0
Угу, можно вообще список сделать и fold для него запилить.
CHayT 07.07.2021 16:48 # 0
bormand 07.07.2021 16:49 # 0
Да почему? Обычный product type. Хотя такое обычно туплом называют, конечно, а не списком.
CHayT 07.07.2021 17:03 # 0
j123123 07.07.2021 15:47 # 0
bormand 07.07.2021 16:04 # 0
Я думаю пока можно без него попробовать. Добавить всегда можно будет.
"Ложность" ака "невыводимость" можно будет доказать перебрав все правила и показав, что они не помогают построить такое дерево, к примеру.
К слову, пока это очень похоже на индуктивные типы в coq. Просто тип пока один: "constructible" или как ты там его назовёшь.
1024-- 07.07.2021 14:16 # 0
(1 + 2) + (1 + 2) обеспечивает кучу вариантов
1. левая замена
2. средняя замена
3. правая замена
4. 1/2/3 и левая/средняя/правая замена где угодно
5. 1/2/3 и левая/средняя/правая замена там, где ещё не заменяли
6. одновременная замена 2 выражений
7. одновременная замена 3 выражений
Дальше строим кучу разных операторов
1. замена с памятью/без памяти (с памятью убеждается, что создаются уникальные идентификаторы, а не совпадающие - x->x1 vs x->x)
2. вилка: замена без памяти, удлиняющая выражение (например, x -> x+x)
3. сход: замена, сокращающая выражение (например, x+x -> x)
4. итерация до достижения неподвижной точки
Дальше определяем числа, скажем, как
0. левая замена
1. правая
2. левая, затем правая
3. правая, затем правая
(или ещё как-то красиво)
Потом ещё находим выражения, на которых так определённые числа можно посчитать.
j123123 07.07.2021 15:29 # +1
Да, ты можешь построить например брейнфак.
сначала идет код программы типа последовательности из "< > + - . [ ]" и там еще будет маркер "^" который означает текущий instruction pointer.
Потом разделитель "#" и дальше будет счетчик для квадратных скобок "[ ]" чтобы находить пару.
Потом опять разделитель "#" и будет как бесконечное поле из чисел от 0 до 255 с маркером, которое нулями слева и справа дописывается
Потом опять разделитель "#" и будет стандартный вывод
например если программа "+ + . > > [ > > ]" то начальное состояние будет
PolinaAksenova 07.07.2021 16:07 # 0
MAKAKA 08.07.2021 01:21 # 0
CHayT 07.07.2021 13:12 # +1
PolinaAksenova 07.07.2021 16:03 # 0
booratihno 08.07.2021 14:12 # +5
грустно
guest6 08.07.2021 14:34 # +2
bormand 08.07.2021 14:59 # +2
CHayT 08.07.2021 15:15 # +3
Hijikata 10.07.2021 18:33 # +2
1024-- 12.07.2021 20:45 # 0
Та же задача о рюкзаке из простого алгоритма превращается в пердолинг с пожиранием памяти.
booratihno 08.07.2021 15:27 # 0
Вот например: когда вы делаете malloc, глибц растит вам секцию кучи (делает brk). Но если вы делаете ОЧЕ большой маллок (выше M_MMAP_THRESHOLD, mallopt(3)) то маллок делает вам анянянямный ммап.
Такие отдельные секции удобнее выпёздывать на мороз по мере их освобождения (а усекновение секции кучи можно делать только с жопы), зато анянямные секции обязаны были выравнены по страничкам
тут мы сначала видим sbrk, а потом mmap (в strace)
в /proc/<pid>/maps мы видим сначала растущий [heap], а потом анонимный регион
bormand 08.07.2021 17:23 # 0
booratihno 08.07.2021 17:31 # 0
но оно там делает дырку
хип кончается на 01e9f000 (32108544)
анонимн регион начина на 7f4ef327b000(139977063641088)
довольно дохуя, не?
(хорошо на x64 жить)
bormand 08.07.2021 17:32 # 0
Если все большие аллокации уходят няверх -- наверное норм.
booratihno 08.07.2021 17:37 # 0
мне вот интересно, нахуя вообще это всё? брк, хип, указатели на code и data, которые там реально в mm_struct..
Почему нельзя было просто поддержать какое-то количество регионов с разными пермишеннами, и всё?
Зачем ядру вообще что-то знать про хип-хуип?
В пинде же вроде VirtualAlloc просто создает какую-то запись VAD, и течет
А уже поверх можно создавать хипы (причем дохуя хипов)
bormand 08.07.2021 17:41 # 0
booratihno 08.07.2021 17:46 # 0
Во всяком случае в классическом System V хак с mmapом не использовали, про него Морис не пишет.
Но БЗД уже тоже да, причем опёнок по другой причине
Old implementations were all sbrk(2) based. In OpenBSD 3.8, Thierry Deval rewrote malloc to use the mmap(2) system call, making the page addresses returned by malloc random
>можно и полностью в юзермоде эмулировать
Ну вот наскока я понимаю, виндовый ``CreateHeap`` так примерно и делает.
Правда vmmap каким-то чудом знает, какой регион (кстати, как он правильно называется у винды? address range?) это хип
https://tr1.cbsistatic.com/hub/i/2010/01/06/7fab9293-c3b4-11e2-bc00-02911874f8c8/Jan-2010-WSTips20f5-Post2FigA.jpg
вон скока хипов, причем один еще и шарбл
bormand 08.07.2021 17:49 # 0
Да поди знает где табличку хипов подсмотреть. Виндбг так то тоже её тоже читать умеет.
booratihno 08.07.2021 17:55 # 0
bormand 08.07.2021 17:59 # 0
booratihno 08.07.2021 18:09 # 0
Было бы круто добавить в сишку такую API: malloc с как-бы ареной. Но не вручную её создавать, а делегатить операционке
(В glibc есть арена, но она не про то)
bormand 08.07.2021 19:23 # 0
MAKAKA 08.07.2021 20:59 # 0
В пинде есть еще анклав какой-то..
Кстати, проверил: malloc на пинде срёт в heap (увеличивая его до неебических размеров), а явный VirtualAlloc создает "private" (ну или какую закажешь) address range.
Ренджи на пинде можно еще смотреть через kernel debugger: У !process (который показывает EPROCESS) есть поле "VDA root", которое адрес корня бинарного дерева, где хранятся VDA (у прыщей вроде есть еще linked list к дереву, а у NT только дерево), и потом по !vda можно его смотреть.
К сожалению, у меня нет пинды с поддержкой kernel debug, шоб проверить
зы: у обычного процесса еще можно посмотреть свои мапы через ``VirtualQuery``
j123123 08.07.2021 21:41 # 0
MAKAKA 08.07.2021 21:52 # 0
на линуксе есть анонимный ``mmap``, на windows есть ``CreateHeap``: они создают отдельные регионы памяти, которые потом можно целиком анмапнуть или удалить
bormand 08.07.2021 22:12 # +1
Именно поэтому я за контроллеры.
j123123 08.07.2021 22:19 # 0
Так mmap в линуксе это сискол, а CreateHeap это какая-то винапи-хуитень. Тебе наверное надо NtAllocateVirtualMemory
Или NtAllocateUserPhysicalPages
Зачем они столько хуйни в винде понаделали?
j123123 08.07.2021 22:26 # 0
NtAllocateUserPhysicalPages
NtAllocateUserPhysicalPagesEx
NtAllocateVirtualMemory
NtAllocateVirtualMemoryEx
NtFlushVirtualMemory
NtFreeVirtualMemory
NtFreeUserPhysicalPages
NtLockVirtualMemory
NtProtectVirtualMemory
NtQueryVirtualMemory
NtReadVirtualMemory
Сколько же хуйни
MAKAKA 08.07.2021 23:06 # 0
MAKAKA 08.07.2021 22:28 # 0
Зачем -- это вопрос к Дэвиду Катлеру, но работает именно так.
В линуксе новый регион создается через mmap (ну или shmget), а в винде через VirtualAlloc.
Но CreateHeap более высокоуровневый, позволяет не думать про конкретные VDA, их мапинг на страницы итд
MAKAKA 08.07.2021 23:00 # 0
На сей раз на прыще
``mmap`` c ``MAP_ANON | MAP_PRIVATE`` возвращает адрес, который хорошо виден в ``/proc/[pid]/map``, и регион там анонимный
``malloc``, как было сказано выше, либо увеличивает регион ``[heap]``, либо создает новый, если область памяти слишком велика.
Сравним с FreeBSD:
Анонимный ``mmap`` требует ``-1`` в качестве fd, иначе возвращает invalid arguments (прыщи работают и так).
Удобная утилита ``procstat`` (жаль, что на прыще такого нет) показывает ренджи памяти, правда пометки ``heap`` там нет: регион, как регион
Если сравнить два региона
то в аутпуте они будут рядышком, но mmap намного дальше хипа (сначала хип, потом mmap)
---
Фряша обссыкивает sbrk:
The brk() and sbrk() functions are legacy interfaces from before the ad-
vent of modern virtual memory management. They are deprecated and not
present on the arm64 or riscv architectures. The mmap(2) interface
should be used to allocate pages instead.
Traditionally, allocators have used sbrk(2) to obtain memory, which is
suboptimal for several reasons, including race conditions, increased
fragmentation, and artificial limitations on maximum usable memory. If
sbrk(2) is supported by the operating system, this allocator uses both
mmap(2) and sbrk(2), in that order of preference; otherwise only
mmap(2) is used.
MAKAKA 08.07.2021 23:08 # +1
Компания просит своих пользователей срочно обновить их.
Фирма по кибербезопасности Sangfor случайно опубликовала инструкцию, где говорится, как с помощью диспетчера печати Windows удаленно получить доступ к другому компьютеру. Jбновления, которые устраняют эту уязвимость, Microsoft уже выпустила.
bormand 08.07.2021 23:21 # 0
Блин, вот реально, все сервисы от мс надо блочить нахер.
З.Ы. Причем вроде диспетчер печати в десятке уже засендбоксен был... Или не весь?
guest6 08.07.2021 23:46 # 0
На семерке он работает от "System"
Ну и вероятно слушает RPC порт для named pipes, чо
MAKAKA 09.07.2021 00:19 # 0
CHayT 10.07.2021 18:46 # +2
http://joeyh.name/blog/entry/a_bitter_pill_for_Microsoft_Copilot/
bormand 10.07.2021 23:38 # 0
CHayT 10.07.2021 23:55 # 0
bormand 11.07.2021 00:19 # 0
MAKAKA 11.07.2021 00:02 # +1