Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

perfect discrimination tree fixes (weight + trace) #48

Open
petarvukmirovic opened this issue Jul 25, 2019 · 2 comments
Open

perfect discrimination tree fixes (weight + trace) #48

petarvukmirovic opened this issue Jul 25, 2019 · 2 comments
Assignees
@petarvukmirovic
Labels
D-medium medium difficulty I-core-types core data types and data structures I-perf performance related issues

Comments

@petarvukmirovic
Copy link
Collaborator

No description provided.

@c-cube c-cube added D-medium medium difficulty I-core-types core data types and data structures I-perf performance related issues labels Jul 25, 2019
@petarvukmirovic
Copy link
Collaborator Author

In HOL (even if you are limited only to pattern matching), larger terms can match smaller ones :

^[x,y,z]. F x z y matches ^[x,y,z]. G x

To circumvent this problem, there is a simple solution: do not calculate the actual exact weight, but whenever you have an applied variable you act as if it was a variable (and do not count argument terms). Also, to deal with eta-normalization, we consider all terms eta-expanded. However, we do not directly eta-expand them but just add the weight of extra db variables as needed.

@petarvukmirovic
Copy link
Collaborator Author

I am on it today.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@petarvukmirovic petarvukmirovic

Labels
D-medium medium difficulty I-core-types core data types and data structures I-perf performance related issues
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@c-cube @petarvukmirovic