Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
12 changes: 6 additions & 6 deletions Mathlib/Computability/PostTuringMachine.lean
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ computation. These are the parameters for the language:

All of these variables denote "essentially finite" types, but for technical reasons it is
convenient to allow them to be infinite anyway. When using an infinite type, we will be interested
to prove that only finitely many values of the type are ever interacted with.
in proving that only finitely many values of the type are ever interacted with.

Given these parameters, there are a few common structures for the model that arise:

Expand Down Expand Up @@ -378,7 +378,7 @@ def step (M : Machine Γ Λ) : Cfg Γ Λ → Option (Cfg Γ Λ) :=
| Stmt.write a => T.write a⟩

/-- The statement `Reaches M s₁ s₂` means that `s₂` is obtained
starting from `s₁` after a finite number of steps from `s₂`. -/
starting from `s₁` after a finite number of steps. -/
def Reaches (M : Machine Γ Λ) : Cfg Γ Λ → Cfg Γ Λ → Prop := ReflTransGen fun a b ↦ b ∈ step M a

/-- The initial configuration. -/
Expand Down Expand Up @@ -825,9 +825,9 @@ Because our construction in the previous section reducing `TM1` to `TM0` doesn't
alphabet, we can do the alphabet reduction on `TM1` instead of `TM0` directly.

The basic idea is to use a bijection between `Γ` and a subset of `Vector Bool n`, where `n` is a
fixed constant. Each tape element is represented as a block of `n` bools. Whenever the machine
fixed constant. Each tape element is represented as a block of `n` `Bool`s. Whenever the machine
wants to read a symbol from the tape, it traverses over the block, performing `n` `branch`
instructions to each any of the `2^n` results.
instructions to reach any of the `2^n` results.

For the `write` instruction, we have to use a `goto` because we need to follow a different code
path depending on the local state, which is not available in the TM1 model, so instead we jump to
Expand Down Expand Up @@ -891,7 +891,7 @@ then return to the original position with `n` moves to the left. -/
def read (f : Γ → Stmt Bool (Λ' Γ Λ σ) σ) : Stmt Bool (Λ' Γ Λ σ) σ :=
readAux n fun v ↦ move n Dir.left <| f (dec v)

/-- Write a list of bools on the tape. -/
/-- Write a list of `Bool`s on the tape. -/
def write : List Bool → Stmt Bool (Λ' Γ Λ σ) σ → Stmt Bool (Λ' Γ Λ σ) σ
| [], q => q
| a :: l, q => (Stmt.write fun _ _ ↦ a) <| Stmt.move Dir.right <| write l q
Expand Down Expand Up @@ -1167,7 +1167,7 @@ end TM1to1

To establish that TM0 and TM1 are equivalent computational models, we must also have a TM0 emulator
in TM1. The main complication here is that TM0 allows an action to depend on the value at the head
and local state, while TM1 doesn't (in order to have more programming language-like semantics).
and local state, while TM1 does not (in order to have more programming language-like semantics).
So we use a computed `goto` to go to a state that performs the desired action and then returns to
normal execution.

Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Computability/TuringMachine.lean
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ computation. These are the parameters for the language:

All of these variables denote "essentially finite" types, but for technical reasons it is
convenient to allow them to be infinite anyway. When using an infinite type, we will be interested
to prove that only finitely many values of the type are ever interacted with.
in proving that only finitely many values of the type are ever interacted with.

Given these parameters, there are a few common structures for the model that arise:

Expand Down Expand Up @@ -117,7 +117,7 @@ variable (σ : Type*)
/-- The TM2 model removes the tape entirely from the TM1 model,
replacing it with an arbitrary (finite) collection of stacks.
The operation `push` puts an element on one of the stacks,
and `pop` removes an element from a stack (and modifying the
and `pop` removes an element from a stack (and modifies the
internal state based on the result). `peek` modifies the
internal state but does not remove an element. -/
inductive Stmt
Expand Down Expand Up @@ -488,7 +488,7 @@ theorem step_run {k : K} (q : TM2.Stmt Γ Λ σ) (v : σ) (S : ∀ k, List (Γ k

end

/-- The translation of TM2 statements to TM1 statements. regular actions have direct equivalents,
/-- The translation of TM2 statements to TM1 statements. Regular actions have direct equivalents,
but stack actions are deferred by going to the corresponding `go` state, so that we can find the
appropriate stack top. -/
def trNormal : TM2.Stmt Γ Λ σ → TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
Expand Down