12
Załóżmy, że chcesz znaleźć program λ nazębnego, T, który spełnia następujące równania:Jakie są najnowocześniejsze metody rozwiązywania równań funkcjonalnych?
(T (λ f x . x)) = (λ a t . a)
(T (λ f x . (f x))) = (λ a t . (t a))
(T (λ f x . (f (f x)))) = (λ a b t . (t a b))
(T (λ f x . (f (f (f x)))) = (λ a b c t . (t a b c))
w tej sprawie, mam ręcznie znaleźć tego rozwiązania:
T = (λ t . (t (λ b c d . (b (λ e . (c e d)))) (λ b . b) (λ b . b)))
Czy istnieje jakąkolwiek strategię rozwiązywania równań z rachunku λ automatycznie? Jaki jest stan wiedzy na ten temat?
Jakiego pojęcia równości używasz tutaj? – dfeuer
[Computational equality] (http://ncatlab.org/nlab/show/equality) *. Przeczytaj "a = b", ponieważ "a" beta redukuje się do "b", w mocnej, normalnej formie. – MaiaVictor
Podczas gdy uważam, że twoje pytanie jest interesujące, nie sądzę, że jest to dobre rozwiązanie do przepełnienia stosu. Jeśli pytasz o algorytmy, powinieneś zapytać na [computer science.SE]. Jak na to pytanie, twoje pytanie nie dotyczy programowania, ale projektowania algorytmów i jest zbyt szerokie, aby można było odpowiedzieć na SO (ostateczną odpowiedzią na twoje pytanie będzie książka/zestawy książek). – Bakuriu