The Inf function in the system F
David, René
HAL, hal-00385177 / Harvested from HAL
Text on HAL
We give a lambda-term of type Nat, Nat->Nat in the system F that computes the minimum of 2 Church numerals in time O(inf.log(inf)). This refutes a conjecture of the "lambda folklore".
Publié le : 1994-05-18
Classification:  [MATH.MATH-LO]Mathematics [math]/Logic [math.LO],  [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 
@article{hal-00385177,
     author = {David, Ren\'e},
     title = {The Inf function in the system F},
     journal = {HAL},
     volume = {1994},
     number = {0},
     year = {1994},
     language = {en},
     url = {http://dml.mathdoc.fr/item/hal-00385177}
}

David, René. The Inf function in the system F. HAL, Tome 1994 (1994) no. 0, . http://gdmltest.u-ga.fr/item/hal-00385177/