12
Si supponga di voler trovare un programma λ-calcolo, T, che soddisfa le seguenti equazioni:Quali sono i metodi più avanzati per la risoluzione di equazioni funzionali?
(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))
In questo caso, ho trovato manualmente questa soluzione:
T = (λ t . (t (λ b c d . (b (λ e . (c e d)))) (λ b . b) (λ b . b)))
C'è qualsiasi strategia per risolvere automaticamente tali equazioni di λ-calcolo? Qual è lo stato dell'arte su questo argomento?
Quale nozione di uguaglianza stai usando qui? – dfeuer
[Equality computazionale] (http://ncatlab.org/nlab/show/equality) *. Si prega di leggere 'a = b' come' a' beta si riduce a 'b', in una forma normale forte. – MaiaVictor
Mentre trovo la tua domanda interessante, non penso che questo sia adatto per Stack Overflow. Se stai chiedendo degli algoritmi dovresti chiedere a [computer science.SE]. Così com'è, la tua domanda non sembra sulla programmazione ma sulla progettazione dell'algoritmo ed è troppo ampia per essere risolta su SO (una risposta definitiva alla tua domanda sarebbe un libro/serie di libri). – Bakuriu