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?

+3

Quale nozione di uguaglianza stai usando qui? – dfeuer

+1

[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

+2

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

risposta

3

In generale, higher order unification è indecidibile, quindi non è possibile sperare in una procedura generale per trovare soluzioni a questi tipi di equazioni.

C'è stata una quantità significativa di lavoro per trovare soluzioni a tali problemi, ma non so di nessuno che dia la risposta al tuo particolare problema. Alcuni buoni riferimenti sono riassunti in questa risposta: Higher-order unification

9

Non sono sicuro dello stato dell'arte, ma il lavoro di William E Byrd sugli interpreti relazionali (come this paper) consente la sintesi di questo tipo di programma.

Vedere anche il suo PolyConf talk per alcune cose interessanti sulla ricerca di termini del programma. I tuoi esempi sembrano come se fossero abbastanza facili da esprimere in quel modo.