Riduzione ß e calcolo lambda

[Dani9210]

Salve a tutti, nel mio corso stiamo facendo il calcolo lambda e sto impazzendo nel capire questo esercizio, devo fare la riduzione beta fino alla forma normale di questo :

((λq.λp.p ≥ 3 ? ((q q) (p − 1)) ∗ p: p)(λq.λp.p ≥ 3 ? ((q q) (p − 1)) ∗ p: p)) 4

non ho la minima idea di come partire, sul libro fa un esempio alquanto sciocco purtroppo.... grazie in anticipo

[hamming_burst]

"Dani9210":
((λq.λp.p ≥ 3 ? ((q q) (p − 1)) ∗ p: p)(λq.λp.p ≥ 3 ? ((q q) (p − 1)) ∗ p: p)) 4

in questa formula sono inserite delle meta-variabili che non hanno un significato semantico esplicitato.
$>=$,$\*$, $-$ sono rispettivamente: geq, prod e minus che sono facilmente recuperabili in formulazione classica del lambda-calcolo.

invece $?$ e $:$, se sono esplicitate dal tuo libro poco si può fare, possono avere qualunque significato quindi uno step applicativo con loro rimarrà indeterminato. Quindi domando: cosa annotano $?$ e $:$

i $:$ potrei intuire ad uno sostituzione di variabili...difficilmente saranno dei tipi.

PS: calcolo lambda, riduzione beta orrore sonoro e grafico...si chiama lambda-calcolo ($\lambda$-calcolo) e beta-riduzione ($\beta$-riduzione).

[perplesso1]

"hamming_burst":Quindi domando: cosa annotano ? e :

Non me ne intendo però butto lì un'idea... non è che che significano then ... else ... ? Nel caso l'espressione sarebbe facile da ridurre perchè se tu poni $W = (λq.λp.p ≥ 3 ? ((q q) (p − 1)) ∗ p: p)$ hai

$WW4 = (WW3)*4 = ((WW2)*3)*4 = 2*3*4 = 24$

Insomma è una ricorsione... ho detto una boiata?

[hamming_burst]

"perplesso":[quote="hamming_burst"]Quindi domando: cosa annotano ? e :

Non me ne intendo però butto lì un'idea... non è che che significano then ... else ... ?
[/quote]
sì, molto probabile. Sono andato a cercar chissà che significato.

Ma:

"perplesso":
Nel caso l'espressione sarebbe facile da ridurre

questo dipende molto dal tipo di semantica e dalla strategia normalizzante.

Ad alto livello sì è semplice, ma se l'if-then-else è definito in modo particolare allora la forma normale potrebbe cambiare e non ritornare quel valore. Cmq probabile sia tutto abb semplice e si utilizzi la strategia leftmost-outermost, quindi il risultato che hai trovato penso sia valido, ma non ho provato.