Обсуждение:Церковное кодирование

Взолнованный

Следующее обсуждение было перенесено сюда из Talk:Church numeral в результате объединения той страницы с этой. -- Дэвид Уолер (обсуждение) 15:53, 25 октября 2005 (UTC) [ ответить ]

Пример схемы

Не является ли реализация схемы обратной?

То есть, не должно ли быть так:

(определить ноль (лямбда (f) (лямбда (x) x)))(определите один (лямбда (f) (лямбда (x) (fx))))(определить два (лямбда (f) (лямбда (x) (f (fx)))))(определить три (лямбда (f) (лямбда (x) (f (f (fx))))))

Это соответствовало бы и пояснительному тексту в верхней части страницы, и Haskell, не говоря уже о примерах, приведенных на странице исчисления лямбда . На самом деле, зачем делать его таким сложным для чтения? Просто скажите:

(определить (ноль f) (лямбда (x) x))(определить (один f) (лямбда (x) (fx)))(определить (два f) (лямбда (x) (f (fx))))(определить (три f) (лямбда (x) (f (f (fx)))))

Примеры, не относящиеся к церкви, также становятся менее туманными:

(определить (add1 x) (+ x 1))(определить (unchurch c) ((c add1) 0))

Однако я не вижу, что добавляет пример схемы в этот момент. Haskell уже чист и, прежде всего, соответствует английскому тексту. Кроме того, Haskell позволяет вам определить все целые числа церкви одним махом, тогда как пример схемы показывает только несколько примеров (потому что эквивалент схемы функции "церковь" просто слишком уродлив).

Выкиньте эту схему. Она ничего не добавляет к статье и только мешает понять, что такое церковные цифры.

  • Согласен со стиранием примера схемы. Он хуже, чем Haskell. Если кто-то хочет сделать это в чистом лямбда-исчислении, это было бы стоящим делом. Brighterorange 16:40, 2 июня 2005 (UTC)

Я не знаю Haskell, и не знаю никого, кто знает Haskell. Я даже не знаю наверняка, что такое Haskell. Scheme я понимаю. Он существует уже давно и хорошо понятен. -- Тони Сидауэй, выступление 18:25, 4 августа 2005 (UTC) [ ответить ]

Пример Scheme должен быть добавлен... Я бы также хотел пойти немного дальше, показав, как выглядит сложение и умножение чисел Чёрча. Сотни студентов знакомятся с этой концепцией каждый год с помощью Scheme (хотя бы через книгу Абельсона и Сассмана, используемую в 6.001 в MIT) -- для меня не имеет смысла не иметь примеров Scheme и некоторого обсуждения вместе с ними. --Cityintherain 02:47, 29 июня 2006 (UTC) [ ответить ]

Существует два возможных кодирования церковных цифр; в одном случае функция-преемник является первым параметром, в другом первым принимается нулевое значение. Я думаю, что в статье следует просто дать версии лямбда-исчисления и позволить студентам каждого языка сделать собственные переводы по мере необходимости. -- bmills 21:37, 24 октября 2005 (UTC) [ ответить ]

Код haskell здесь *ужасный*. Хотя код scheme "добавляет" less, весь смысл добавления "less" в том, что он делает базовые концепции более понятными для тех, у кого еще нет полного понимания или кому нужно напомнить об этом в 3 часа ночи, когда он пьян и спорит с кем-то о чем-то, о чем он не думал годами — scheme намеренно "проста". Как есть, аргумент можно привести в пользу C. Код haskell опирается на несколько DWIM haskell, так что перевод на язык, который не является haskell, опирается на очень специфическое знание правил каррирования и заключения в скобки Haskell , что *не* является функцией для статьи в энциклопедии "получить подсказку" (хакеры haskell, пожалуйста, прекратите это делать; это не первый раз, когда я вижу простую концепцию, завуалированную "посмотрите, как прекрасен haskell?"). Код схемы для church/unchurch, который явно представляет собой лямбда-исчисление с одним аргументом, со всеми скобками на нужных местах, выглядит следующим образом:

(определить (церковь сущ.) (если (ноль? n) (лямбда (ф)(лямбда (х) х))) (лямбда (ф)(лямбда (х) (ж (((церковь (- н 1)) ж) х))))))(определить (нецерковный сущ.) ((н (лямбда (x) (+ x 1))) 0))

Остальное оставлено в качестве упражнения, если этого еще нет в истории статьи. Кто-нибудь менее раздраженный, чем я, пожалуйста, не стесняйтесь перерабатывать статью по мере необходимости, чтобы получить то, что кажется более разумным, чем то, что написано.--66.92.73.217 07:23, 15 августа 2006 (UTC) [ ответить ]


Я не вижу причин, почему бы не включить код Scheme. Возможно, среди читателей этой статьи есть те, кто не знает Haskell, но знает Scheme. Однако я бы переформатировал приведенный выше код Scheme в более читабельную форму, например:

(определить (натуральное-число->церковное-числительное n) (если (ноль? n) (лямбда (ф) (лямбда (х) х))) (лямбда (ф) (лямбда (х) (ф (((натуральное-число->церковное-числительное (- н 1)) ф) х))))))(определить (церковное-число->натуральное-число n) ((n (лямбда (x) (+ x 1))) 0))
Jos.koot ( обсуждение ) 16:22, 1 апреля 2009 (UTC) [ ответ ]

Имя

Я думаю, что эта статья должна называться «Church numerals»; это название мы всегда используем в школе. Church «integer» неверно, потому что эта кодировка представляет только натуральные числа, а не целые числа (которые могут быть отрицательными). Есть ли какой-то исторический прецедент для «church integers»? Brighterorange 16:40, 2 июня 2005 (UTC)

Ну, это должно быть "Church numeral" (единственное число), насколько я понимаю правила Википедии. Удивительно, что кто-то, по-видимому, изобрел такой ошибочный термин, как "Church integer" и перенаправил с ранее правильного названия! (Это своего рода numal , определенно не целое число , черт возьми.) Проблема в том, что теперь есть миллиард ссылок на неправильное название, и я слишком новичок в редактировании, чтобы знать, как исправить их все экономически. --res ( Talk ) 17:36:15, 2005-08-04 (UTC)
Поскольку изучение церковных числительных обычно также включает другие церковные кодировки (например, церковные булевы значения ), а концепции одной из них значительно помогают пониманию других, я предлагаю объединить эту страницу с церковной кодировкой . -- bmills 21:39, 24 октября 2005 (UTC) [ ответить ]

Функции Хаскеля

Функции Haskell элегантны. Но я не могу не заметить, что если вы используете расширенный Haskell, вы можете записать типы как

церковь :: Целое число -> (forall a. Церковь a)unchurch :: (forall a. Church a) -> Integer

Это показывает изоморфизм (на самом деле, с натуральными числами, а не с целыми) немного яснее. Но тогда другие могут пожаловаться, что это (еще) не Haskell. — Ashley Y 11:33, 2 декабря 2005 (UTC) [ ответить ]

Я сам больше сторонник ML, но разве оба варианта не одинаковы? forall a. Church a просто устраняет ограничение prenex для типа функции, если в Haskell вообще есть ограничение prenex. Я не думаю, что это имеет какое-либо значение в любом случае. -- bmills 22:30, 4 декабря 2005 (UTC) [ ответить ]
Сигнатура типа для "church" точно такая же, как вы говорите, а вот для unchurch — нет. (church,unchurch) не является изоморфизмом между натуральными числами и "Church Integer", но является изоморфизмом между натуральными числами и "forall a. Church a". Однако я не собираюсь ее менять. — Эшли Y 10:38, 5 декабря 2005 (UTC) [ ответить ]

Связь с нумерацией Гёделя

Вступление гласит: «Многие студенты-математики знакомы с нумерацией Гёделя членов множества; кодирование Чёрча — эквивалентная операция, определённая на абстракциях лямбда вместо натуральных чисел». Разве это не запутывает всё без нужды? Что означает слово «эквивалентный»? Я думаю, лучше удалить это предложение. — Lambiam Talk 07:15, 16 ноября 2006 (UTC) [ ответить ]

Согласен. Сравнение с арифметикой Пеано выглядит лучше. —Предыдущий неподписанный комментарий добавлен 67.188.108.234 (обсуждение) 06:45, 3 июля 2010 (UTC) [ ответить ]

Внешние реализации

Я написал Python- реализацию списков Чёрча с использованием функций высшего порядка, когда мне было скучно. Не стесняйтесь ссылаться на неё, если хотите. --Ertugrul S. (обс.) 01:26, 26 января 2009 (UTC) [ ответить ]

Нулевой предикат

Термин (\n.((n(\xF))(\xT))) [n], где [n] — это число Чёрча для n, равен T, если n равно нулю, а F — n не равно нулю. Не следует ли добавить предикат Zero?=\n.((n(\xF))(\xT)) к числовым функциям, таким как Plus, Pred и т. д.? Jos.koot ( talk ) 10:17, 1 апреля 2009 (UTC) [ reply ]

Каррирование

Разве функции здесь не должны быть такими же, как в статье по лямбда-исчислению? Phantom Hoover ( обсуждение ) 14:44, 19 декабря 2009 (UTC) [ ответить ]

Упоминать аксиомы Пеано?

Связаны ли аксиомы Пеано с кодировками Чёрча для чисел и сложения? Если да, то на них следует хотя бы ссылаться. —Предыдущий неподписанный комментарий добавлен Indil ( talk • contribs ) 04:27, 12 мая 2011 (UTC) [ ответить ]

Добавлено объяснение предшественника

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

Thepigdog ( обсуждение ) 05:30, 3 ноября 2013 (UTC) [ ответить ]

Очистить

Я рассматриваю некоторые косметические изменения на этой странице, чтобы написать лямбда-исчисление с использованием Extension:Math - MediaWiki. Если кто-то испытывает сильную привязанность к текущему макету, пожалуйста, сообщите мне, и я откажусь. Мне очень нравится опция MathJax в настройках для отображения математики. У меня никогда не было с ней проблем, и она намного понятнее. Кроме того, она масштабируется, когда вы нажимаете на нее :). Я использую x\ y для приложения, что выглядит хорошо, но немного громоздко для написания.

Thepigdog ( обсуждение ) 17:26, 4 декабря 2013 (UTC) [ ответить ]

Деление и отрицательные числа

Я добавил деление и числа со знаком. Это перебор с точки зрения демонстрации тезиса Чёрча-Тьюринга, но некоторым людям, похоже, интересно, как можно реализовать отрицательные числа. Лучший источник, который я нашел о числах со знаком, это:

  • представление-отрицательных-и-комплексных-чисел-с-помощью-лямбда-исчисления

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

Лучшее, что я нашел по теме «Разделение», — это сайт Ллойда Эллисона.

  • Лямбда-исчисление целые числа

Его реализация DIVMOD позволяет определять как делитель, так и остаток. Я не использовал именно это определение, потому что его сложнее понять, и оно использует MINUS ( MONUS ) дважды, что требует много бета-сокращений. Однако данное мной описание не кажется мне таким уж хорошим. Я подумаю над этим.

Thepigdog ( обсуждение ) 12:29, 25 марта 2014 (UTC) [ ответить ]

Здравствуйте, уважаемые википедисты!

Я только что изменил одну внешнюю ссылку на кодировку Church . Пожалуйста, уделите немного времени, чтобы просмотреть мои правки. Если у вас есть какие-либо вопросы или вам нужно, чтобы бот игнорировал ссылки или страницу в целом, посетите этот простой раздел FaQ для получения дополнительной информации. Я внес следующие изменения:

  • Добавлен архив https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf в http://tromp.github.io/cl/LC.pdf

Когда вы закончите просматривать мои изменения, пожалуйста, установите отмеченный параметр ниже на значение true или failed, чтобы сообщить об этом другим (документация по адресу ).{{Sourcecheck}}

проверятьY Редактор проверил эту правку и исправил все обнаруженные ошибки.

  • Если вы обнаружили URL-адреса, которые бот ошибочно посчитал неработающими, вы можете сообщить о них с помощью этого инструмента.
  • Если вы обнаружили ошибку в архивах или самих URL-адресах, вы можете исправить их с помощью этого инструмента.

Привет.— InternetArchiveBot ( Сообщить об ошибке ) 14:12, 24 ноября 2016 (UTC) [ ответить ]

Операторы булевой логики, закодированные Чёрчем n o t 1 {\displaystyle not_{1}} и n o t 2 {\displaystyle not_{2}}

Кто-то поднял вопрос о двух определениях для логического отрицания в #haskell, говоря об определениях и в этом разделе . n o t 1 {\displaystyle not_{1}} n o t 2 {\displaystyle not_{2}}

Никто, похоже, не знал, почему их было два, и определения, похоже, работали и в haskell, и в python, так что я не понимаю разницы. Похоже, это не имеет ничего общего со строгим и ленивым — в отличие от того, что, похоже, говорится в примечаниях — поскольку оба работают и в строгом, и в ленивом языке.

Буду очень признателен за разъяснения или исправления статьи. 2A02:1810:2505:BF00:EC76:4D29:7CE7:51FB (обсуждение) 23:19, 23 декабря 2018 (UTC)anon [ ответить ]

Согласен, примечания определенно неверны. Я их удаляю, и если между ними есть существенные фактические различия, их можно будет добавить в будущем. Ebf526 ( talk ) 01:02, 20 июля 2021 (UTC) [ ответить ]

Церковное деление чисел

Существует [1] гораздо меньший термин для деления:

 делим = \n.\m.\f.\xn (\x.\ff x) (\dx) (n (\tm (\x.\ff x) (\cf (ct)) (\xx)) x)

Ссылки

  1. ^ https://github.com/tromp/AIT/blob/master/div.lam

Слишком много представлений списка

Я думаю, что представление «Две пары как узел списка» можно было бы исключить.

Кодировку Скотта следует считать стандартным представлением, правое сворачивание представляет интерес само по себе, а «отдельная пара как узел списка» достигает наибольшей общей простоты.

По сравнению с последним, «Две пары как узел списка» кажется просто неоправданно сложным во всех отношениях.

Retrieved from "https://en.wikipedia.org/w/index.php?title=Talk:Church_encoding&oldid=1206688834"