dowsing icon indicating copy to clipboard operation
dowsing copied to clipboard
verified publisher icon Drup

TODO List

Open Drup opened this issue 4 years ago • 1 comments

Software engineering

  • [x] Add tests
  • [x] Implement a proper notion of printing environment
  • [x] Use proper logging
  • [x] Plug together the unification and the database again

Science

  • [ ] Make sure the returned unifiers are minimal
  • [x] Add rigid variables

Indexation:

  • [x] Head
  • [x] Nb of arguments ("Equal" or "At least")
  • [ ] Variances of constants
  • [ ] Term indexing: To Read:
    • http://wwwlehre.dhbw-stuttgart.de/~sschulz/PAPERS/Schulz2013-FVI.pdf
    • Fingerprint Indexing for Paramodulation and Rewriting

Drup avatar Jan 20 '21 18:01 Drup

Reading list and/or references

  • [RDC]: Di Cosmo (Roberto). - Isomorphisms of types: from lambda-calculus to information retrieval and language design. - Birkhauser, 1994.

  • [Rit90] Mikael Rittri. Retrieving library identifiers by equational matching of types in 10th Int. Conf. on Automated Deduction. Lecture Notes in Computer Science, 449, July 1990.

  • [Rit91] Mikael Rittri. Using types as search keys in func- tion libraries. Journal of Functional Programming, 1(1):71- 89, 1991.

Unification

  • [Rit93] Mikael Rittri. Retrieving library functions by unifying types modulo linear isomorphism. RAIRO Theoretical Informatics and Applications, 27(6):523-540, 1993.

  • [DJ90]

  • Equality [SE94]

With modules

  • [Mul; ZW93] ADC96; ADCD97

Serialization

To speed up database deserialization, we could use a format that allows random access in an mmap datastructure. Example of such formats:

Drup avatar Nov 04 '21 14:11 Drup