Comment modéliser la sortie du calcul lambda binaire?

Question

Je suis en train d'écrire un interprète pour John Tromp's binary lambda calculus

Je code écrit pour effectuer les opérations suivantes:

1. Parse l'entrée binaire dans une structure de données représentant le typées régulier lambda-calcul
2. Beta-reduce ce terme

Que se passe-t-il alors?

• Comment la "sortie" est-elle interprétée?
• est la sortie
  • a) le terme résultant retraduite en binaire via le même encodage,
  • ou b) le flux binaire codé par une liste de booléens Faux terminé?
• (Et ce qui se passe si la sortie ne forme pas une telle liste?)

Ou que je comprends mal comment BLC fonctionne?

Answer 1

Je suggère d'utiliser http://www.ioccc.org/2012/tromp/hint.html comme référence principale. La page Wikipedia est probablement très bien, mais ses notes originales sur BLC sont plutôt bonnes.

Sur le thème de l'entrée et de sortie, il a ceci à dire:

Plus précisément, il définit une machine universelle, qui, à partir d'un flux de bits d'entrée, analyse le codage binaire d'un calcul lambda term, applique cela au reste de l'entrée (traduit en une liste paresseuse de booléens, qui ont une représentation standard en lambda calcul), et traduit le résultat évalué en un flux de bits à sortir.