C'è un calcolo SKI digitato?

Question

La maggior parte di noi conosce la corrispondenza tra e lambda calcolo . Ma non ho mai visto (abbastanza in profondità forse non ho guardato) l'equivalente di "combinatori digitati", corrispondente al lambda calcolo semplicemente digitato. Fa cosa del genere esiste? Dove si poteva trovare informazioni su di esso?

Answer 1

La completezza espressiva dei combinatori digitati rispetto al lambda calcolo semplicemente digitato è stato dimostrato . Per ogni combinatore non tipizzato, si ha la necessità di una intera famiglia di combinatori digitati. Ad esempio, si ha

• $ \ mathbf {I} _ {\ alpha \ a \ alpha} $
• $ \ mathbf {K} _ {\ alpha \ a (\ beta \ a \ alpha)} $
• $ \ mathbf {S} _ {\ alpha \ a (\ beta \ a \ gamma) \ a (\ alpha \ a \ beta \ a (\ alpha \ a \ gamma))} $

per tutte le combinazioni di tipi semplici $ \ alpha, \ beta $ e $ \ gamma $.

In alternativa, basti pensare alle tipologie come schemi di tipo (o tipi polimorfi) e metterle in Haskell e voilà: combinatori .