Найдите функции Хаскелла f, g такие, что fg = f.г - PullRequest
Новая
       77

Найдите функции Хаскелла f, g такие, что fg = f.г

0 голосов
/ 26 января 2019

Изучая Haskell, я столкнулся с проблемой найти две функции f и g, такие, что f g и f . g эквивалентны (и всего, поэтому такие вещи, как f = undefined или f = (.) f don не в счет). Данное решение состоит в том, что f и g оба равны \x -> x . x (или join (.)).

(отмечу, что это не характерно для Хаскелла; это можно выразить в чистой комбинаторной логике как «найди f и g такие, что f g = B f g», и данное решение будет затем преобразовано в f = g = W B.)

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

  • f g = f . g (дано)
  • f g z = (f . g) z (eta-расширение обеих сторон)
  • f g z = f (g z) (упрощение RHS)

И я не знаю, как действовать дальше. Что я буду делать дальше, пытаясь найти решение?

1 Ответ

0 голосов
/ 26 января 2019

Я обнаружил, что можно найти семейство решений, рассмотрев вычисление церковных чисел.В церковном кодировании умножение выполняется путем составления церковных чисел, а возведение в степень - путем применения базы к показателю степени.Таким образом, если f является церковной кодировкой некоторого числа x, а g является церковной кодировкой некоторого числа y, то f g = f . g подразумевает y^x = x*y.Любые неотрицательные целочисленные решения этого уравнения переводятся в решения исходной задачи.Примеры:

  • x=1, y=0, f=id, g=const id
  • x=1, y=1, f=id, g=id
  • x=1, y=2, f=id, g=join (.)
  • Так как y^1 = y = 1*y для всех y, он делаетощущение, что f=id работает для всех церковных цифр g.Это действительно так, и на самом деле, как отметил Рейн Хенрикс, это верно для всех g, и это легко проверить осмотром.
  • x=2, y=0, f=join (.), g=const id
  • x=2, y=2, f=join (.), g=join (.)
  • x=3, y=0, f=(.) <*> join (.), g=const id
  • Поскольку 0^x = 0 = x*0 для всех положительных x, имеет смысл, что g=const id работает для всех положительных церковных чисел f.(Это не работает для f=const id, церковная цифра 0, что имеет смысл, поскольку 0^0 является неопределенной формой.)
...