Проблема получения Y-комбинатора из определения указателя исправления - PullRequest
Новая
       88

Проблема получения Y-комбинатора из определения указателя исправления

2 голосов
/ 21 октября 2019

Моя проблема: я хочу получить Y-комбинатор из определения точки фиксации 

(define Y1
    (lambda (f)
        (f (Y1 f))))

Мой процесс подтверждения здесь: https://gist.github.com/jiamo/f865bc8a9d921deb1ccf5df03fe9f9dc

(Мой метод вождения исходит от https://mvanier.livejournal.com/2897.html Но начнем с определения точки фиксации, а не с конкретной функции факта)

Наконец я хочу увидеть равенство этих двух функций (Y14, Y15). Но я не могу его найтиout. 

(define Y14
  (lambda (g)
    (g (((lambda (h) (lambda (g) (g ((h h) g))))
        (lambda (h) (lambda (g) (g ((h h) g))))) g))))

;; g use both outside and inside change outside g to f 

(define Y14
  (lambda (f)
    (f (((lambda (h) (lambda (g) (g ((h h) g))))
        (lambda (h) (lambda (g) (g ((h h) g)))))
        f))))


(define Y15
    (lambda (g)
     ((lambda (h) (g (h h)))
      (lambda (h) (g (h h))))))

------- ОБНОВЛЕНИЕ -------

Я ошибаюсь.

Вhttps://gist.github.com/jiamo/f865bc8a9d921deb1ccf5df03fe9f9dc

(define (Y4 self)
    (lambda (f) ((lambda (g) (f (g f))) (self self))))

Но это может быть (В https://gist.github.com/jiamo/5e21e9c1a044211fc5e3479ec7d3321b):

(define (Y4 self)
    ((lambda (g) (lambda (f) (f (g f))))(self self)))

Тогда оно может дойти до 

(define Y10
   ((lambda (h) ((lambda (g) (lambda (f) (f (g f)))) (h h)))
     (lambda (h) ((lambda (g) (lambda (f) (f (g f)))) (h h)))))

Тогда сделать G = (lambda (g) (lambda (f) (f (g f)))) Мытакже может получить: 

(define Y12
    (lambda (G)
       ((lambda (h) (G (h h)))
        (lambda (h) (G (h h))))))

Таким образом, функция указателя исправления не имеет разницы, чем функция специального факта.

Однако

Моя ошибка имой процесс вождения по происхождению - это правильное вождение. Поэтому вопрос о происхождении может быть здесь и ждать, пока кто-нибудь предложит свои варианты.

...