numerale Chiesa per l'aggiunta

Question

Sono bloccato su al passo successivo. Sarà bello se qualcuno mi può dare una mano:

2 = λfx.f(f x)
3 = λfx.f(f(f x))
ADD = λm n f x. m f (n f x)

I miei passi sono:

   (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
-> ((λn f x. (λf x.f(f(f x))) f (n f x))) (λf x.f(f x))
-> ((λf x. (λf' x'.f'(f'(f' x'))) f ((λf" x".f"(f" x")) f x)

E 'la multa parentesi? Io davvero mi confondo sulle sostituzioni e parentesi. C'è una, tecnica formale più semplice per affrontare tali problemi?

Answer 1

Alligator uova!

Ecco i miei passi, che ho derivato con l'aiuto di Alligator Uova:

ADD 2 3
-> (λm n f x. m f (n f x)) (λf x.f(f(f x))) (λf x.f(f x))
->   (λn f x. (λf x.f(f(f x))) f (n f x))   (λf x.f(f x))
->     (λf x. (λf x.f(f(f x))) f ((λf x.f(f x)) f x)) 
->     (λf x.   (λx.f(f(f x)))   ((λf x.f(f x)) f x)) 
->     (λf x.       f(f(f(λf x.f(f x)) f x)))))
->     (λf x.       f(f(f  (λx.f(f x)) x)))))
->     (λf x.       f(f(f     (f(f x))  )))))

Answer 2

Il mio consiglio, dalla mia esperienza limitata ma recenti:

1. Do una cosa alla volta: eseguire una conversione alfa, una riduzione beta o una conversione eta. Nota a margine della pagina che si sta lavorando su quello che hai preso un passo per raggiungere la linea successiva. Se queste parole non sono familiari a voi, quello che fanno sarà - basta dare un'occhiata su Wikipedia .

Un breve riassunto di questi passaggi di riduzione:

Alpha significa solo cambiare i nomi delle variabili in un contesto coerente:

λfx. f (f x) => λgx. g (g x)

significa solo applicare la Beta lambda su una argomento

(λf x. f x) b => λx. b x

Eta è semplicemente 'scartare' una funzione inutilmente avvolto che il cambiamento doesen't il suo significato.

λx.f x => f

Poi

2. Usa un sacco di alfa conversione di cambiare i nomi delle variabili per rendere le cose più chiare. Tutte quelle fs, è sempre andando a confondere. Hai fatto qualcosa di simile con il " sulla seconda riga

3. finta di essere un computer! Non salto in avanti o saltare un passaggio quando si sta valutando un'espressione. Basta fare la prossima cosa (e solo una cosa). spostare solo più veloce, una volta che siete sicuri si muove lentamente.

4. Si consideri nominare alcune delle espressioni e solo sostituendo le espressioni lambda quando si ha bisogno di valutarli. Io di solito notare la sostituzione a margine della pagina come by def come in realtà non è una fase di riduzione. Qualcosa di simile:

   add two three 
   (λm n f x. m f (n f x)) two three | by def
   

Quindi, seguendo le regole di cui sopra, ecco il mio esempio pratico:

two   = λfx. f (f x)
three = λfx. f (f (f x))
add   = λmnfx. m f (n f x)

0  | add two three 
1  | (λm n f x. m f (n f x)) two three           | by def
2  | (λn f x. two f (n f x)) three               | beta
3  | (λf x. two f (three f x))                   | beta
4  | (λf x. two f ((λfx. f (f (f x))) f x))      | by def
5  | (λf x. two f ((λgy. g (g (g y))) f x))      | alpha
6  | (λf x. two f ((λy. f (f (f y))) x))         | beta
7  | (λf x. two f (f (f (f x))))                 | beta
8  | (λf x. (λfx. f (f x)) f (f (f (f x))))      | by def
9  | (λf x. (λgy. g (g y)) f (f (f (f x))))      | alpha
10 | (λf x. (λy. f (f y)) (f (f (f x))))         | beta
11 | (λf x. (λy. f (f (f (f (f x))))))           | beta

Answer 3

  

C'è una, tecnica formale più semplice per affrontare tali problemi?

È molto più facile scrivere un riduttore e PrettyPrinter per i termini lambda che è di fare riduzioni a mano. Ma PLT Redex può dare una gamba su riduzioni; provare la definizione di regole per la riduzione del normale ordine, e poi tutto quello che dovete fare è preoccuparsi di prettyPrinting i risultati senza parentesi ridondanti .

È probabilmente imparare molto di più, anche.