Une nouvelle C\(\beta\)-réduction dans la logique combinatoire (Q762137)

In this paper we give a new reduction in combinatory logic analogous to \(\lambda\) \(\beta\)-reduction. Such problem has been studied by Curry, Hindley and Seldin. Curry's reduction based on abstraction algorithm \((abc_{\beta}f_{\beta})\) does not solve the problem completely. Hindley in his unpublished notes gives a new definition of equivalence between CL-reduction and \(\lambda\) \(\beta\)-reduction. The CL-reduction that we give is based on Hindley's characterisation of \(C\beta\)-reduction described in his later work. It consists of finding an abstraction algorithm [ ]\({}^ 0\) and a reduction in combinatory logic \(\succ^ 0\) satisfying certain properties. We define [ ]\({}^ 0\) and \(\succ^ 0\) and prove the theorem that the couple ([ ]\({}^ 0,\succ^ 0)\) has these properties.