libhstar

Pure untyped extensional non-deterministic memoized combinator machine.

TODO

• Test infrastructure
  • Collect benchmark problems
  • Specify behavior
  • Build test jig
• Basic reduction
  • Eager linear reduction
  • Memoization
  • Eta reduction as in - [ ]
• Nondeterminism
  • Reduction rules for JOIN
  • Sampling from joins over flat domains
• Todd-Coxeter
  • Forward-chaining merge logic
• Types
  • Reduction rules for basic datatypes
  • Optimizations for basic datatypes (byte operations, integers)
  • Json datatypes: booleans, numbers, strings, lists, dicts
  • Serialization via protobuf, json, etc. (use upb)
• Fast C implementation
  • C implementation
  • Python bindings for c version
  • Define performance metrics
  • Build performance benchmarking jig

References

• [Scott76]
  Dana Scott (1976)
  Datatypes as Lattices
• [Hindley08]
  J. Roger Hindley, J.P. Seldin (2008)
  "Lambda calculus and combinatory logic: an introduction"
• [Koopman91]
  Philip Koopman, Peter Lee (1991)
  Architectural considerations for graph reduction
• [Boulifa03]
  Rabea Boulifa, Mohamed Mezghiche (2003)
  Another Implementation Technique for Functional Languages
• [Obermeyer09]
  Fritz Obermeyer (2009)
  Automated Equational Reasoning in Nondeterministic λ-Calculi Modulo Theories H*
• [Fischer11]
  Sebastian Fischer, Oleg Kiselyov, Chung-Chieh Shan (2011)
  Purely functional lazy nondeterministic programming

License

Copyright (c) 2016 Fritz Obermeyer.

Libhstar is licensed under the Apache 2.0 License.