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

Solution Visualisations #14

Merged
merged 4 commits into from
Apr 5, 2024
Merged

Solution Visualisations #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3839156
Visualisation & Vincular Cont.
stella-mj Apr 1, 2024
08a81ab
Merge remote-tracking branch 'upstream/main' into visualisation
stella-mj Apr 1, 2024
5a21a9b
Visualisations for Classic & Vincular Containment
stella-mj Apr 3, 2024
df81869
Edit to vincular shading method
stella-mj Apr 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
78 changes: 56 additions & 22 deletions combined.essence
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,8 @@ given length : int
find perm : sequence (size length, injective) of int(1..length)
find permPadded : matrix indexed by [int(0..length+1)] of int(0..length+1)




given classic_avoidance : set of sequence of int


such that
forAll pattern in classic_avoidance .
!(exists ix : matrix indexed by [int(1..|pattern|)] of int(1..length) .
Expand All @@ -17,39 +13,77 @@ such that
pattern(n1) < pattern(n2) <-> perm(ix[n1]) < perm(ix[n2])))


given classic_containment : sequence of sequence of int
find classic_containment_evidence : sequence (size |classic_containment|) of sequence (maxSize length) of int(1..length)
find patterns : sequence (size |classic_containment|) of sequence (maxSize length) of int(1..length)

$ the length of the evidence needs to match the length of the pattern
such that
[ |ix| = |pattern|
| (patternId, pattern) <- classic_containment
, letting ix be classic_containment_evidence(patternId)
]

given classic_containment : set of sequence of int

$ ...
such that
[ forAll n1, n2 : int(1..|pattern|) . n1 < n2 -> ix(n1) < ix(n2)
| (patternId, pattern) <- classic_containment
, letting ix be classic_containment_evidence(patternId)
]

$ if two points are ordered in a particular way in the pattern
$ they must also be ordered in the same way in the permutation
such that
forAll pattern in classic_containment .
(exists ix : matrix indexed by [int(1..|pattern|)] of int(1..length) .
(forAll i,j : int(1..|pattern|) . i < j -> ix[i] < ix[j]) /\
(forAll n1, n2 : int(1..|pattern|) , n1 < n2 .
pattern(n1) < pattern(n2) <-> perm(ix[n1]) < perm(ix[n2])))
[ forAll n1, n2 : int(1..|pattern|) , n1 < n2 .
pattern(n1) < pattern(n2) <-> perm(ix(n1)) < perm(ix(n2))
| (patternId, pattern) <- classic_containment
, letting ix be classic_containment_evidence(patternId)
]

such that
patterns = classic_containment


$ such that
$ forAll pattern in classic_containment .
$ (exists ix : matrix indexed by [int(1..|pattern|)] of int(1..length) .
$ (forAll i,j : int(1..|pattern|) . i < j -> ix[i] < ix[j]) /\
$ (forAll n1, n2 : int(1..|pattern|) , n1 < n2 .
$ pattern(n1) < pattern(n2) <-> perm(ix[n1]) < perm(ix[n2])))


given vincular_containment : set of (sequence (injective) of int, set of int)
given vincular_containment : sequence of (sequence (injective) of int, set of int)

find vincular_containment_evidence : sequence (size |vincular_containment|) of sequence (maxSize length) of int(1..length)

$ the length of the evidence needs to match the length of the pattern
such that
forAll (pattern, bars) in vincular_containment .
exists ix : matrix indexed by [int(1..|pattern|)] of int(1..length)

, (forAll i,j : int(1..|pattern|) . i < j -> ix[i] < ix[j]) /\
$ n1 and n2 are indices
(forAll n1, n2 : int(1..|pattern|) , n1 < n2 .
(pattern(n1) < pattern(n2) <-> perm(ix[n1]) < perm(ix[n2]))
)
[ |ix| = |pattern|
| (patternId, (pattern, bars)) <- vincular_containment
, letting ix be vincular_containment_evidence(patternId)
]

.
such that
[ forAll n : int(1..|pattern|-1) . ix(n) < ix(n+1)
| (patternId, (pattern, bars)) <- vincular_containment
, letting ix be vincular_containment_evidence(patternId)
]

(forAll bar in bars . ix[bar] + 1 = ix[bar+1])
such that
[ forAll n1, n2 : int(1..|pattern|) , n1 < n2 .
(pattern(n1) < pattern(n2) <-> perm(ix(n1)) < perm(ix(n2)))
| (patternId, (pattern, bars)) <- vincular_containment
, letting ix be vincular_containment_evidence(patternId)
]

such that
[ forAll bar in bars . ix(bar) + 1 = ix(bar+1)
| (patternId, (pattern, bars)) <- vincular_containment
, letting ix be vincular_containment_evidence(patternId)
]


branching on [perm]


given vincular_avoidance : set of (sequence (injective) of int, set of int)
Expand Down
Loading