Телеграмм чат группы rust_offtopic страница 19578

badtrousers

когда пропозиции разворачиваются одна в другую

Да нет, оно сводится к юниту

f f f

разворачиваем левые и правые f

unit f unit

разворачиваем правило x f y

unit

00:44пожаловаться #1

Или

f f f

разворачиваем f f справа по правилу f x

f unit

разворачиваем снова по правилу f x

unit

00:44пожаловаться #2

badtrousers

или как я сказал бы это ложное ощущение

У тебя у самого есть рабочий прототип? Ты пробовал на нём писать что-то нетривиальное?

00:45пожаловаться #3

ну ты понимаешь что если ты можешь в общем случае доказывать

00:45пожаловаться #4

Emmanuel Goldstein

Или

f f f

разворачиваем f f справа по правилу f x

f unit

разворачиваем снова по правилу f x

unit

что это будет одна и та же самая редукция

00:45пожаловаться #5

то ты решил halting problem?

00:45пожаловаться #6

В общем случае это не будет одна и та же редукция, естественно

00:45пожаловаться #7

я понимаю

00:45пожаловаться #8

Это просто минимальное воспроизведение неоднозначных фраз

00:46пожаловаться #9

ну вот если есть вопрос будет ли какое–то решение сводиться к одному не в зависимости от логических переменных

00:46пожаловаться #10

как мультисат

00:46пожаловаться #11

3SAT ведь уже NP–complete

00:46пожаловаться #12

Emmanuel Goldstein

У тебя у самого есть рабочий прототип? Ты пробовал на нём писать что-то нетривиальное?

да

00:46пожаловаться #13

мы при помощи логоса оцифровываем юридическую документацию

00:47пожаловаться #14

Ну ок
Жду демок

00:47пожаловаться #15

pdf -> ocr -> duct -> logos -> графовая база

00:47пожаловаться #16

badtrousers

pdf -> ocr -> duct -> logos -> графовая база

Ну тут это скорее язык представления, не?

00:47пожаловаться #17

А не язык программирования

00:47пожаловаться #18

логос и не является языком программирования

00:47пожаловаться #19

(Кстати, я пока не могу тривиально доказать, что он Тьюринг-полный)