Code

Determinization#24

Code

Merged

maxsnew merged 28 commits intomainmaxsnew/grammars-and-semantic-actions:mainfrom determinize-refactormaxsnew/grammars-and-semantic-actions:determinize-refactorCopy head branch name to clipboardOct 8, 2024

+1,757-885

Commits

Commits on Sep 29, 2024

• work on determinization

  nvarner

  committed
  e48adfb

Commits on Oct 1, 2024

• Revised determinization attempt

  nvarner

  committed
  60efb87

• push the sketch of equivalence for the day

  stschaef

  committed
  aeed4c3

Commits on Oct 2, 2024

• DFA Traces are equiv to string

  stschaef

  committed
  6612559

Commits on Oct 4, 2024

• DFA defs update to use inductives

  stschaef

  committed
  e5d8385

• nfa to dfa

  stschaef

  committed
  1b94c89

• need to fix indexed inductives

  stschaef

  committed
  88a5bf8

Commits on Oct 5, 2024

• Merge branch 'main' into determinize-refactor

  stschaef

  committed
  9bd23c9

• impute lifts, use new inductives

  stschaef

  committed
  e9268fb

• need to refactor the epsilon closed sets to be nonempty

  stschaef

  committed
  40a277d

• Need to induct on walks. Mostly reduced to choice fcns, walk combinators,

  stschaef

  committed
  667e1ce

Commits on Oct 6, 2024

• Mostly show that ordering on FinSet gives FinOrd

  nvarner

  committed
  265c9b6

• an inductive graph walk allows the def of the linear term

  stschaef

  committed
  462b092

• inductive reachability

  stschaef

  committed
  0ef04cd

• added postulates for graph walk being a (Fin)Set

  stschaef

  committed
  0d63f45

• Reduced determinization to 4 holes

  stschaef

  committed
  9153a3e

Commits on Oct 7, 2024

• levels for DFAs and NFAs

  stschaef

  committed
  add8d31

• reduced to just the choice functions

  stschaef

  committed
  d048736

• simplify dfa to nfa

  stschaef

  committed
  2ea9698

• graph walks form a finite order

  stschaef

  committed
  9b171d3

Commits on Oct 8, 2024

• GraphPath is finitely ordered

  stschaef

  committed
  0334e3d

• one more hole for choosing an accepting state

  stschaef

  committed
  c90973d

• Determinization is done

  stschaef

  committed
  442c616

• add the logical equivalence between NFA/Powerset DFA as an explicit thm

  maxsnew

  committed
  2ad4d1e

• naming

  maxsnew

  committed
  a647e57

• fix the NFA=~DFA code by using the old defn of NFAs

  maxsnew

  committed
  87e553a

• comment out broken determinization2 code

  maxsnew

  committed
  f970f71

• most whitespace fixes

  maxsnew

  committed
  d1eaef4