È possibile implementare `max` efficientemente sul calcolo lambda non tipizzato?

Question

min è di solito definito sul lambda calcolo non tipizzata come (usando Caramel's syntax):

sub a b = (b pred a) 
<= a b = (is_zero (sub b a)) 
min a b = (<= a b a b) 

Questo è terribilmente inefficiente. Sub è quadratico, poiché si applica pred (che è lineare) b volte. C'è un'implementazione molto più efficiente di min come:

min a b succ zero = (a a_succ (const zero) (b b_succ (const zero)))) 
    a_succ pred cont = (cont pred) 
    b_succ pred cont = (succ (cont pred)) 

Questo zip attraverso entrambi i numeri in stile continuation passaggio fino a raggiungere il primo zero. Ora, sto cercando di trovare una max che è efficiente come min, che ha le seguenti proprietà:

1. a e b vengono utilizzati più di una volta sul corpo della funzione.

2. Ha una forma normale beta (vale a dire, non utilizza i combinatori a virgola fissa è fortemente normalizzante).

Esiste la definizione max?

Answer 1

Solo per i record, se a e b può essere utilizzato due volte (cioè, si tratterebbe di un nodo dup sulle reti di interazione), c'è una soluzione semplice:

true a b = a 
false a b = b 
const a b = a 

-- less than or equal 
lte a b = (go a true (go b false)) 
    go = (num result -> (num (pred cont -> (cont pred)) (const result))) 

min = (a b -> (lte a b a b)) 
max = (a b -> (lte a b b a)) 

-- A simple test 
main = (max (max 3 14) (max 2 13)) 

Ma non richiedeva alcuna duplicazione (cioè, lte a b b a non è consentito) quindi non so ancora se è possibile.