Results about finite space and regular languages - #180

Draft

crei wants to merge 59 commits into

mainfrom

Commits on Mar 10, 2026

Update Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

crei
and
chenson2018
authored
cb9e7a3
Extract common parts.
crei
committed
cc78278
Simplify definitions and proofs.
crei
committed
07d7bcd
Use "@[expose] public section"
crei
committed
841be7f
Update Cslib.lean
crei
committed
abac0f1
Add missed file.
crei
committed
ae6c498

Commits on Mar 19, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
b38b929
fix import.
crei
committed
7401a21

Commits on Apr 30, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
93b6704
Move "expose" command below module-level documentation.
crei
committed
3110f77

Commits on Jun 2, 2026

Commits on Jun 4, 2026

Do not use BiTape for input.
crei
committed
3d406b7

Commits on Jun 5, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
398ad91
Make move optional.
crei
committed
6847a62

Commits on Jun 10, 2026

feat(Governance): Add new area maintainers for algorithms and logic (#610)

fmontesi
and
arademaker
authored
82e06e3
chore(Semantics/LTS/Bisimulation): golf and simplify (#613)

thomaskwaring
and
twwar
authored
b9d8076

Commits on Jun 11, 2026

Add chenson2018 explicitly to logic CODEOWNERS
fmontesi
authored
edfa974
feat: logical equivalence for modal logic (#535)

fmontesi
and
chenson2018
authored
e3991ff
doc: prefer +/- for Boolean `optConfig` (#620)
chenson2018
authored
616e04b

Commits on Jun 12, 2026

chore: bump mathlib to 8589236, fix breaking changes (#628)

mathlib-nightly-testing[bot]
and
chenson2018
authored
1f601a2
feat(Data/PFunctor): add free monad of a polynomial functor (#477)

quangvdao
and
cursoragent
authored
d6c0b90

Commits on Jun 13, 2026

chore: bump mathlib to 73b2611, fix breaking changes (#640)

mathlib-nightly-testing[bot]
and
chenson2018
authored
ee5567b
chore: split the `Relation` module (#632)
chenson2018
authored
d5148c0
doc: add wikidata attribute for Church-Rosser theorems (#626)
chenson2018
authored
6311ef1
chore(LTS): add API for TraceEq and relatives (#617)

thomaskwaring
and
twwar
authored
87c249d

Commits on Jun 15, 2026

chore: bump toolchain to v4.31.0 (#651)
Garmelon
authored
8ea71c8

Commits on Jun 16, 2026

refactor(Logics/Propositional): classical and intuitionistic inference systems (#536)

thomaskwaring
and
twwar
authored
70c5bf5

Commits on Jun 19, 2026

Commits on Jun 20, 2026

feat(LocallyNameless/Untyped): `subst_intro` weaker precondition (#666)

lengyijun
and
chenson2018
authored
dc23a39

Commits on Jun 21, 2026

Commits on Jun 22, 2026

chore: bump mathlib to 29af524, fix breaking changes (#670)

mathlib-nightly-testing[bot]
and
chenson2018
authored
dbce0f9
feat(untyped): define CBN and Standard evaluation strategies (#671)

m-ow
and
chenson2018
authored
f10c049

Commits on Jun 23, 2026

Merge remote-tracking branch 'origin/main' into multi-tape-tm
crei
committed
085e658
More design notes, references, switch from BiTape to \int -> Nat and make step function total.
crei
committed
4f6cf21
Some small tweaks.
crei
committed
d4a14ef

Commits on Jun 25, 2026

feat(Automata): Transducers (#650)
fmontesi
authored
a441db6

Commits on Jun 26, 2026

chore: fix the header of Cslib/Computability/Automata/DA/Prod.lean (#682)
ctchou
authored
2772f42

Commits on Jul 1, 2026

chore: disable .github/workflows/lake-update.yml on personal forks (#686)
ctchou
authored
1edb390

Commits on Jul 2, 2026

chore: bump mathlib to d52d26f, fix breaking changes (#694)

mathlib-nightly-testing[bot]
and
chenson2018
authored
5c41dcf

Commits on Jul 5, 2026

fix(Foundations/Syntax): guard substitution notation with noWs (#687)
loafer-19
authored
7940a10

Commits on Jul 6, 2026

feat(Machines): Single-Tape Nondeterministic Turing Machines (NTMs) (#683)
fmontesi
authored
f2aeae5

Commits on Jul 9, 2026

feat(untyped): standardization theorem for the lambda calculus (#679)

m-ow
and
chenson2018
authored
27d53d7
feat(LocallyNameless/Untyped): new theorem `lcAt_le` (#699)

lengyijun
and
chenson2018
authored
c0120dd

Commits on Jul 11, 2026

Commits on Jul 12, 2026

Commits on Jul 19, 2026

updates
crei
committed
4a149e2