Repository navigation
Expand file tree
/
Copy pathComputabilityEquivalence.lean
More file actions
54 lines (52 loc) · 2.7 KB
/
Copy pathComputabilityEquivalence.lean
File metadata and controls
54 lines (52 loc) · 2.7 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
import ComputabilityEquivalence.Equivalence
import ComputabilityEquivalence.Models.MarkovBounds
import ComputabilityEquivalence.Models.MarkovComp
import ComputabilityEquivalence.Models.MarkovTM0
import ComputabilityEquivalence.Models.MarkovTM0Support
import ComputabilityEquivalence.Models.MarkovTM1
import ComputabilityEquivalence.Models.PartrecToTM2
import ComputabilityEquivalence.Models.PartrecTM2ToTM1
import ComputabilityEquivalence.Models.MarkovFlatten
import ComputabilityEquivalence.Models.TrListDecode
import ComputabilityEquivalence.Models.MarkovTM0Completeness
import ComputabilityEquivalence.Models.PartrecMarkovIff
import ComputabilityEquivalence.Models.ReplicateCode
import ComputabilityEquivalence.Models.MarkovScanEmit
import ComputabilityEquivalence.Models.PartrecIOWrap
import ComputabilityEquivalence.Models.PartrecDecoder
import ComputabilityEquivalence.Models.PartrecGlue
import ComputabilityEquivalence.Models.PartrecMarkovFinal
import ComputabilityEquivalence.MarkovCorollaries
import ComputabilityEquivalence.RegisterPartrec
import ComputabilityEquivalence.Models.RegisterReaches
import ComputabilityEquivalence.Models.RegisterBlocks
import ComputabilityEquivalence.Models.RegisterStraight
import ComputabilityEquivalence.Models.RegisterSplit
import ComputabilityEquivalence.Models.RegisterComp
import ComputabilityEquivalence.Models.RegisterPrec
import ComputabilityEquivalence.Models.RegisterRfind
import ComputabilityEquivalence.Models.RegisterCompile
import ComputabilityEquivalence.Models.DetlovsBlocks
import ComputabilityEquivalence.Models.DetlovsSolo
import ComputabilityEquivalence.Models.DetlovsLeaves
import ComputabilityEquivalence.Models.DetlovsRelocate
import ComputabilityEquivalence.Models.DetlovsRegions
import ComputabilityEquivalence.Models.DetlovsFetch
import ComputabilityEquivalence.Models.DetlovsReflect
import ComputabilityEquivalence.Models.DetlovsWiden
import ComputabilityEquivalence.Models.DetlovsComp
import ComputabilityEquivalence.Models.DetlovsCompRun
import ComputabilityEquivalence.Models.DetlovsCompChain
import ComputabilityEquivalence.Models.DetlovsCompAssemble
import ComputabilityEquivalence.Models.DetlovsPrec
import ComputabilityEquivalence.Models.DetlovsRfind
import ComputabilityEquivalence.Models.DetlovsAssemble
import ComputabilityEquivalence.Models.DetlovsMarkov
/-!
# Markov normal algorithms ⇔ partial recursive functions
Root module: imports the whole development. The equivalence is packaged as
`markovSpoke : PartrecSpoke MarkovComputes`, with the compilation direction
proved twice — by machine simulation (`Models/PartrecMarkovFinal.lean`) and
by the Detlovs-faithful constructor-induction compiler
(`Models/DetlovsMarkov.lean`). See `README.md` and `docs/ARCHITECTURE.md`.
-/