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

Implement -> #511

Closed
4 of 6 tasks
Tracked by #510
niklasdewally opened this issue Nov 28, 2024 · 4 comments · Fixed by #597 or #608
Closed
4 of 6 tasks
Tracked by #510

Implement -> #511

niklasdewally opened this issue Nov 28, 2024 · 4 comments · Fixed by #597 or #608
Assignees
@niklasdewally
Labels
area::rules Related to rewrite rules kind::feature New feature or request

Comments

@niklasdewally
Copy link
Collaborator

niklasdewally commented Nov 28, 2024 •
edited
Loading

Implement material implication, ->.

To-do

Note: many of the rules below are usually bidirectional, but I choose to apply them in the direction that makes terms syntactically simpler or easier to pass to Minion.

Normalisation rules:

  • !q -> !p ~> p -> q (contraposition)
  • p -> (q -> r) ~> (p /\ q) -> r (import export)
  • !(p->q) ~> p /\ !q (negation)

Tautologies:

  • p -> p ~> true (reflexivity)
  • (p->q) \/ (q->p) ~> true (totality)
  • (p->q) \/ (p-> !q) ~> true (conditional excluded middle)

See also
@niklasdewally niklasdewally mentioned this issue Nov 28, 2024
Open
6 tasks
@niklasdewally niklasdewally self-assigned this Nov 28, 2024
@niklasdewally niklasdewally added area::rules Related to rewrite rules kind::feature New feature or request labels Nov 28, 2024
This was referenced Jan 14, 2025
Merged
Merged
@niklasdewally niklasdewally linked a pull request Jan 20, 2025 that will close this issue
feat(rules): add implication normalisation rules #597
Merged
@ozgurakgun
Copy link
Contributor

What about the last two checkboxes in the original message then? Did you decide they are not needed?

@ozgurakgun
Copy link
Contributor

I mean they are clearly not needed for correctness or completeness, but could make sense as optimisations.

@niklasdewally
Copy link
Collaborator Author

What about the last two checkboxes in the original message then? Did you decide they are not needed?

I am wary of the cost of checking pairs of elements in an or for these properties, so decided against doing them (for now)

Also seems that savile row doesn't do them either.

@ozgurakgun
Copy link
Contributor

I was interested to see if / how often they would fire, especially because I know SR doesn't do them :)

@niklasdewally niklasdewally reopened this Jan 20, 2025
niklasdewally added a commit that referenced this issue Jan 21, 2025
@niklasdewally
feat(rules): add more -> tautologies to the partial evaluator
cd8d8b9 
Add the following implication tautologies to the partial evaluator:

  + Totality: `(p->q) \/ (q->p) ~> true`

  + Conditional excluded middle: `(p->q) \/ (p-> !q) ~> true`

These tautologies both involve checking pairs of an `or`. I originally
thought checking pairs was too expensive, so did not implement them.

Primarily, Savile Row does not check these, so us adding them here is a
good experiment to see how useful they are. Given the frequency of
complex conditionals in modelling, it is likely to give some sort of
benefit.

The implementation in this commit does not change the time complexity to
check disjunctions that do not contain implications - this is still
O(n).

Issue: #511
@niklasdewally niklasdewally mentioned this issue Jan 21, 2025
Merged
niklasdewally added a commit that referenced this issue Jan 21, 2025
@niklasdewally
feat(rules): add more -> tautologies to the partial evaluator
4b3cd13 
Add the following implication tautologies to the partial evaluator:

  + Totality: `(p->q) \/ (q->p) ~> true`

  + Conditional excluded middle: `(p->q) \/ (p-> !q) ~> true`

These tautologies both involve checking pairs of an `or`. I originally
thought checking pairs was too expensive, so did not implement them.

Primarily, Savile Row does not check these, so adding them here is a
good experiment to see how useful they are. Given the frequency of
complex conditionals in modelling, it is likely to give some sort of
benefit.

The implementation in this commit does not change the time complexity to
check disjunctions that do not contain implications - this is still
O(n).

Issue: #511
niklasdewally added a commit that referenced this issue Jan 21, 2025
@niklasdewally
feat(rules): add more -> tautologies to the partial evaluator
eb4384b 
Add the following implication tautologies to the partial evaluator:

  + Totality: `(p->q) \/ (q->p) ~> true`

  + Conditional excluded middle: `(p->q) \/ (p-> !q) ~> true`

These tautologies both involve checking pairs inside an `or`. I
originally thought checking pairs was too expensive, so did not
implement them.

Primarily, Savile Row does not check these, so adding them here is a
good experiment to see how useful they are. Given the frequency of
complex conditionals in modelling, it is likely to give some sort of
benefit.

The implementation in this commit does not change the time complexity to
check disjunctions that do not contain implications - this is still
O(n).

Issue: #511
@niklasdewally niklasdewally linked a pull request Jan 21, 2025 that will close this issue
feat(rules): add more -> tautologies to the partial evaluator #608
Merged
niklasdewally added a commit that referenced this issue Jan 21, 2025
@niklasdewally
feat(rules): add more -> tautologies to the partial evaluator
c5b7f3c 
Add the following implication tautologies to the partial evaluator:

  + Totality: `(p->q) \/ (q->p) ~> true`

  + Conditional excluded middle: `(p->q) \/ (p-> !q) ~> true`

These tautologies both involve checking pairs inside an `or`. I
originally thought checking pairs was too expensive, so did not
implement them.

Primarily, Savile Row does not check these, so adding them here is a
good experiment to see how useful they are. Given the frequency of
complex conditionals in modelling, it is likely to give some sort of
benefit.

The implementation in this commit does not change the time complexity to
check disjunctions that do not contain implications - this is still
O(n).

Issue: #511
niklasdewally added a commit that referenced this issue Jan 21, 2025
@niklasdewally
feat(rules): add more -> tautologies to the partial evaluator
53b5ddb 
Add the following implication tautologies to the partial evaluator:

  + Totality: `(p->q) \/ (q->p) ~> true`

  + Conditional excluded middle: `(p->q) \/ (p-> !q) ~> true`

These tautologies both involve checking pairs inside an `or`. I
originally thought checking pairs was too expensive, so did not
implement them.

Primarily, Savile Row does not check these, so adding them here is a
good experiment to see how useful they are. Given the frequency of
complex conditionals in modelling, it is likely to give some sort of
benefit.

The implementation in this commit does not change the time complexity to
check disjunctions that do not contain implications - this is still
O(n).

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

@niklasdewally niklasdewally

Labels
area::rules Related to rewrite rules kind::feature New feature or request
Projects
None yet
Milestone
No milestone
2 participants
@ozgurakgun @niklasdewally