diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 25e526df..40be325f 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -15,8 +15,8 @@ jobs: steps: - uses: actions/checkout@v4 - uses: leanprover/lean-action@v1 - with: - build-args: "--wfail --iofail" + # with: + # build-args: "--iofail" - name: "lake exe mk_all --check --module" run: | set -e diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml index ff26c85c..0ee57fc0 100644 --- a/.github/workflows/pr-title.yml +++ b/.github/workflows/pr-title.yml @@ -17,7 +17,3 @@ jobs: with: script: | const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message; - console.log(`Message: ${msg}`) - if (!/^(ci|feat|fix|doc|style|refactor|test|chore|perf)(\(.*\))?: .*[^.]($|\n\n)/.test(msg)) { - core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).'); - } diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 736ed0d8..e2591bcb 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,3 +1,46 @@ +**Table of Contents** + +- [Contributing to CSLib](#contributing-to-cslib) +- [Contribution model](#contribution-model) +- [Style and documentation](#style-and-documentation) + - [Variable names](#variable-names) + - [Proof style and golfing :golf:](#proof-style-and-golfing-golf) + - [Notation](#notation) + - [Documentation](#documentation) +- [Design principles](#design-principles) + - [Reuse](#reuse) +- [Continuous Integration](#continuous-integration) + - [Pull Request Titles](#pull-request-titles) + - [Testing](#testing) + - [Linting](#linting) + - [Imports](#imports) +- [Getting started](#getting-started) + - [Before you start: coordination to avoid rework](#before-you-start-coordination-to-avoid-rework) + - [Finding tasks](#finding-tasks) + - [Working groups](#working-groups) + - [Proposing a new working group](#proposing-a-new-working-group) + - [Examples of welcome contributions](#examples-of-welcome-contributions) + - [Pillar 1: Formalising Computer Science in Lean](#pillar-1-formalising-computer-science-in-lean) + - [Algorithms and Data Structures](#algorithms-and-data-structures) + - [Verified data structures with time complexity (Batteries + Time Monad)](#verified-data-structures-with-time-complexity-batteries--time-monad) + - [Graph algorithms and graph foundations](#graph-algorithms-and-graph-foundations) + - [APIs for algorithmic paradigms](#apis-for-algorithmic-paradigms) + - [Programming Languages, Models of Computation and Interaction](#programming-languages-models-of-computation-and-interaction) + - [Logics](#logics) + - [Semantics and program equivalences](#semantics-and-program-equivalences) + - [Semantic frameworks](#semantic-frameworks) + - [Program equivalences](#program-equivalences) + - [Pillar 2: Code reasoning](#pillar-2-code-reasoning) + - [Contributing Boole examples](#contributing-boole-examples) + - [Boole specifications](#boole-specifications) + - [Issue labels for Boole](#issue-labels-for-boole) + - [Front ends for Boole](#front-ends-for-boole) + - [Back ends for Boole](#back-ends-for-boole) + - [Implementing verification paradigms](#implementing-verification-paradigms) + - [Lean automation](#lean-automation) + - [The role of AI](#the-role-of-ai) + + # Contributing to CSLib It's great that you're interested in contributing to CSLib! :tada: @@ -12,9 +55,11 @@ Each PR needs to be approved by at least one relevant maintainer. You can read t If you are adding something new to CSLib and are in doubt about it, you are very welcome to contact us on the [Lean prover Zulip chat](https://leanprover.zulipchat.com/). +If you are unfamiliar with CSLib as a whole and want to understand how to get started, please see [Getting started](#getting-started). + # Style and documentation -We generally follow the [mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that as well. Some things worth mentioning and conventions specific to this library are explained next. +We generally follow the [mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that as well. Some things worth mentioning and conventions specific to CSLib are explained next. ## Variable names @@ -79,3 +124,208 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The There is a also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by running `lake exe mk_all --module` locally, which will make the required changes. + +# Getting started + +CSLib is a community effort. To understand its scope and vision, please read the [CSLib whitepaper](https://arxiv.org/abs/2602.04846). +For an overview of its technical approach to reuse, continuous integration, and proof automation, please read the [Computer Science as Infrastructure paper](https://arxiv.org/abs/2602.15078). + +Key project links include: + +- Website: https://www.cslib.io/ +- GitHub issues + PRs: https://github.com/leanprover/cslib +- Open contribution board: https://github.com/leanprover/cslib/projects?query=is%3Aopen +- Community discussion (Lean Community Zulip): https://leanprover.zulipchat.com/ + - CSLib channels are the recommended place to coordinate and ask questions. + +## Before you start: coordination to avoid rework + +Most contributions are welcome as straightforward PRs. However, **for any major development**, it is strongly recommended to discuss first on Zulip (or via a GitHub issue) so that the scope, dependencies, and placement in the library are aligned. + +Examples of work that should be discussed first: + +- New cross-cutting abstractions / typeclasses / notation schemes. +- New foundational frameworks. +- Major refactorings. +- New frontend or backend components for CSLib's verification infrastructure. +- Proposals for new working groups (see below). + +## Finding tasks + +If you are looking for a concrete starting point, please look at: + +- The CSLib Zulip channels. +- Our [GitHub issues](https://github.com/leanprover/cslib/issues). + + +## Working groups + +CSLib is structured to support multiple topic-focused efforts. We organise sustained work via **working groups** (informal or formal), which typically have a topic scope and a Zulip topic/channel for coordination. + +If you want to **join** a working group, start by posting on the relevant CSLib Zulip channel describing your background and what you want to contribute. + +### Proposing a new working group + +If you want to propose a new working group, write a short proposal (Zulip message or GitHub issue is fine) that includes: + +- **Topic**: What do you want to do? +- **Execution plan**: What is your execution plan? +- **Collaborators**: If some group or people are already planning to work on the topic, write them. + +The goal is to keep proposals lightweight while ensuring CSLib remains coherent and reusable. + +## Examples of welcome contributions + +Here you can find some (non-exhaustive) examples of topics looking for contributions. + +### Pillar 1: Formalising Computer Science in Lean + +Pillar 1 is about the formalisation of Computer Science as reusable infrastructure. This includes, but is not limited to, models of computation, semantics, logics, algorithms, data structures, metatheory, and supporting mathematics. + +#### Algorithms and Data Structures + +##### Verified data structures with time complexity (Batteries + Time Monad) + +A concrete and high-impact track is to verify implementations and time complexity bounds for [data structures from Batteries](https://github.com/leanprover-community/batteries/tree/main/Batteries/Data). + +Examples of candidate targets: + +- List and Array developments +- Binary heap +- Binomial heap +- Union find +- Red-black trees + +##### Graph algorithms and graph foundations + +- Foundational definitions (directed/undirected simple graphs, etc.) +- Core algorithms and their correctness proofs: + - DFS, topological sorting, SCC + - shortest paths, APSP + - max-flow + - minimum spanning tree + - spanners + - Gomory–Hu trees + +##### APIs for algorithmic paradigms + +Reusable APIs that support many concrete algorithms. + +- Divide-and-conquer + - Master theorem +- Dynamic programming + - generic DP API patterns + - quadrangle inequality (Yao ’80) + - SMAWK algorithm + +#### Programming Languages, Models of Computation and Interaction + +- Automata (on finite and infinite words) +- Choreographic languages +- Lambda calculi +- Petri Nets +- Process calculi, like CCS and pi-calculus +- Frameworks for language encodings (compilers, etc.). +- Proof techniques for the correctness of encodings. + +#### Logics + +We aim at formalising a number of logics of different kinds, including linear logic, modal logics, etc. + +We welcome proofs of logical equivalences and metatheoretical results such as identity expansion, cut elimiation, etc. + +Examples of interesting logics include: +- Linear logic +- Temporal logic +- Separation logic + +#### Semantics and program equivalences + +##### Semantic frameworks +- Denotational semantics +- Operational semantics, including results on labelled transition systems and reduction systems + +##### Program equivalences + +- Bisimulation +- May/Must testing +- Trace equivalence + +### Pillar 2: Code reasoning + +Pillar 2 is about infrastructure for reasoning about code in mainstream programming languages via intermediate representations, VC generation, and automation. + +We are interested in collecting a large number of programs in Boole (see the [CSLib whitepaper](https://arxiv.org/abs/2602.04846) for Boole's vision). + +You can try the Boole sandbox examples at . + +#### Contributing Boole examples + +We are interested in collecting a large number of programs in Boole. + +If you'd like to contribute examples, please propose and coordinate on the [Zulip channel for code reasoning](https://leanprover.zulipchat.com/#narrow/channel/563135-CSLib.3A-Code-Reasoning) first (especially if the example requires new features). + +We separate Boole examples into two directories: + +- examples that work with the current Boole back end +- examples that are broken or contain features not yet implemented + +Contributions to both sets are valuable: working examples demonstrate capabilities; 'broken' examples identify missing features and bottlenecks. + +#### Boole specifications + +Currently, Boole specifications are based on Strata Core: + +A key long-term goal is to support specifications that reference arbitrary Lean concepts, especially those formalised as part of CSLib Pillar 1. Designing this cleanly within the Strata framework is a challenging and valuable project. + +#### Issue labels for Boole + +If you have feature requests for Boole, file an issue with title `feat(Boole): `. + +For bugs, errors, or other issues, file an issue with label `Boole`. + +#### Front ends for Boole + +We are interested in developing translations from real-world programming languages to Boole. + +- Prototype translations are welcome to explore feasibility and identify design constraints. +- If you want to propose a translation for inclusion in CSLib, coordinate on Zulip. + +We expect initial translations will be ad hoc and trusted. The eventual goal is to formalize the semantics of front ends and prove (as a Lean metatheorem) that translations preserve semantics. + +#### Back ends for Boole + +We are interested in building Boole back ends that take as input Boole programs with formal specifications and construct proof obligations in Lean, which, if proved, ensure that the program meets its specification. + +- A prototype translation based on a deep embedding in Strata exists, but is not fully foundational. +- A major long-term goal is to prove Lean meta-theorems showing that proving the verification conditions ensures correctness of the Boole program. + +Alternative directions are welcome, e.g.: + +- Exploring a shallow embedding approach +- Leveraging Loom for more foundational pipelines + +A back end for **time complexity analysis** is also of interest. + +#### Implementing verification paradigms + +The formal methods community has a wide range of verification techniques that could be valuable in the Boole ecosystem, e.g.: + +- proof by refinement +- techniques for program equivalence +- other deductive verification paradigms + +#### Lean automation + +Since Boole back ends reduce correctness questions to Lean conjectures, automation is central. + +We already rely on key techniques such as `grind` and `lean-smt`. Additional work on automation for conjectures generated from Boole is welcome, including domain-specific automation that remains performant and readable. + +#### The role of AI + +There are two primary areas where generative AI can help: + +- generating/refining specifications (at the front-end or Boole level) +- helping to prove Lean conjectures + +Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable. \ No newline at end of file diff --git a/Cslib.lean b/Cslib.lean index 8905be5f..3c8097ae 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -29,6 +29,26 @@ public import Cslib.Computability.Languages.Language public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage +public import Cslib.Computability.Machines.MultiTapeTuring.AddRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.GraphReachability +public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats +public import Cslib.Computability.Machines.MultiTapeTuring.IsZeroRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.IteCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.MoveRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.MulRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension +public import Cslib.Computability.Machines.MultiTapeTuring.WhileCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes +public import Cslib.Computability.Machines.SingleTapeTuring.Basic public import Cslib.Computability.URM.Basic public import Cslib.Computability.URM.Computable public import Cslib.Computability.URM.Defs @@ -39,6 +59,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects public import Cslib.Foundations.Control.Monad.Free.Fold +public import Cslib.Foundations.Data.BiTape public import Cslib.Foundations.Data.FinFun public import Cslib.Foundations.Data.HasFresh public import Cslib.Foundations.Data.Nat.Segment @@ -50,6 +71,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Relation public import Cslib.Foundations.Data.Set.Saturation +public import Cslib.Foundations.Data.StackTape public import Cslib.Foundations.Lint.Basic public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean index bacd41e7..31f05103 100644 --- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean +++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean @@ -17,7 +17,7 @@ public import Mathlib.Data.Nat.Log # MergeSort on a list In this file we introduce `merge` and `mergeSort` algorithms that returns a time monad -over the list `TimeM (List α)`. The time complexity of `mergeSort` is the number of comparisons. +over the list `TimeM ℕ (List α)`. The time complexity of `mergeSort` is the number of comparisons. -- ## Main results @@ -34,8 +34,8 @@ namespace Cslib.Algorithms.Lean.TimeM variable {α : Type} [LinearOrder α] /-- Merges two lists into a single list, counting comparisons as time cost. -Returns a `TimeM (List α)` where the time represents the number of comparisons performed. -/ -def merge : List α → List α → TimeM (List α) +Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/ +def merge : List α → List α → TimeM ℕ (List α) | [], ys => return ys | xs, [] => return xs | x::xs', y::ys' => do @@ -48,8 +48,8 @@ def merge : List α → List α → TimeM (List α) return (y :: rest) /-- Sorts a list using the merge sort algorithm, counting comparisons as time cost. -Returns a `TimeM (List α)` where the time represents the total number of comparisons. -/ -def mergeSort (xs : List α) : TimeM (List α) := do +Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. -/ +def mergeSort (xs : List α) : TimeM ℕ (List α) := do if xs.length < 2 then return xs else let half := xs.length / 2 diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean index d890bd9a..2509e175 100644 --- a/Cslib/Algorithms/Lean/TimeM.lean +++ b/Cslib/Algorithms/Lean/TimeM.lean @@ -7,13 +7,17 @@ Authors: Sorrachai Yingchareonthawornhcai, Eric Wieser module import Cslib.Init +public import Mathlib.Algebra.Group.Defs @[expose] public section /-! # TimeM: Time Complexity Monad -`TimeM α` represents a computation that produces a value of type `α` and tracks its time cost. +`TimeM T α` represents a computation that produces a value of type `α` and tracks its time cost. + +`T` is usually instantiated as `ℕ` to count operations, but can be instantiated as `ℝ` to count +actual wall time, or as more complex types in order to model more general costs. ## Design Principles 1. **Pure inputs, timed outputs**: Functions take plain values and return `TimeM` results @@ -38,60 +42,88 @@ See [Danielsson2008] for the discussion. namespace Cslib.Algorithms.Lean /-- A monad for tracking time complexity of computations. -`TimeM α` represents a computation that returns a value of type `α` -and accumulates a time cost (represented as a natural number). -/ +`TimeM T α` represents a computation that returns a value of type `α` +and accumulates a time cost (represented as a type `T`, typically `ℕ`). -/ @[ext] -structure TimeM (α : Type*) where +structure TimeM (T : Type*) (α : Type*) where /-- The return value of the computation -/ ret : α /-- The accumulated time cost of the computation -/ - time : ℕ + time : T namespace TimeM /-- Lifts a pure value into a `TimeM` computation with zero time cost. Prefer to use `pure` instead of `TimeM.pure`. -/ -protected def pure {α} (a : α) : TimeM α := +protected def pure [Zero T] {α} (a : α) : TimeM T α := ⟨a, 0⟩ +instance [Zero T] : Pure (TimeM T) where + pure := TimeM.pure + /-- Sequentially composes two `TimeM` computations, summing their time costs. Prefer to use the `>>=` notation. -/ -protected def bind {α β} (m : TimeM α) (f : α → TimeM β) : TimeM β := +protected def bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) : TimeM T β := let r := f m.ret ⟨r.ret, m.time + r.time⟩ -instance : Monad TimeM where - pure := TimeM.pure +instance [Add T] : Bind (TimeM T) where bind := TimeM.bind -@[simp, grind =] theorem ret_pure {α} (a : α) : (pure a : TimeM α).ret = a := rfl -@[simp, grind =] theorem ret_bind {α β} (m : TimeM α) (f : α → TimeM β) : - (m >>= f).ret = (f m.ret).ret := rfl -@[simp, grind =] theorem ret_map {α β} (f : α → β) (x : TimeM α) : (f <$> x).ret = f x.ret := rfl -@[simp] theorem ret_seqRight {α} (x y : TimeM α) : (x *> y).ret = y.ret := rfl -@[simp] theorem ret_seqLeft {α} (x y : TimeM α) : (x <* y).ret = x.ret := rfl -@[simp] theorem ret_seq {α β} (f : TimeM (α → β)) (x : TimeM α) : (f <*> x).ret = f.ret x.ret := rfl +instance : Functor (TimeM T) where + map f x := ⟨f x.ret, x.time⟩ -@[simp, grind =] theorem time_bind {α β} (m : TimeM α) (f : α → TimeM β) : - (m >>= f).time = m.time + (f m.ret).time := rfl -@[simp, grind =] theorem time_pure {α} (a : α) : (pure a : TimeM α).time = 0 := rfl -@[simp, grind =] theorem time_map {α β} (f : α → β) (x : TimeM α) : (f <$> x).time = x.time := rfl -@[simp] theorem time_seqRight {α} (x y : TimeM α) : (x *> y).time = x.time + y.time := rfl -@[simp] theorem time_seqLeft {α} (x y : TimeM α) : (x <* y).time = x.time + y.time := rfl -@[simp] theorem time_seq {α β} (f : TimeM (α → β)) (x : TimeM α) : - (f <*> x).time = f.time + x.time := rfl +instance [Add T] : Seq (TimeM T) where + seq f x := ⟨f.ret (x ()).ret, f.time + (x ()).time⟩ + +instance [Add T] : SeqLeft (TimeM T) where + seqLeft x y := ⟨x.ret, x.time + (y ()).time⟩ + +instance [Add T] : SeqRight (TimeM T) where + seqRight x y := ⟨(y ()).ret, x.time + (y ()).time⟩ +instance [AddZero T] : Monad (TimeM T) where + pure := Pure.pure + bind := Bind.bind + map := Functor.map + seq := Seq.seq + seqLeft := SeqLeft.seqLeft + seqRight := SeqRight.seqRight -instance : LawfulMonad TimeM := .mk' +@[simp, grind =] theorem ret_pure {α} [Zero T] (a : α) : (pure a : TimeM T α).ret = a := rfl +@[simp, grind =] theorem ret_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) : + (m >>= f).ret = (f m.ret).ret := rfl +@[simp, grind =] theorem ret_map {α β} (f : α → β) (x : TimeM T α) : (f <$> x).ret = f x.ret := rfl +@[simp] theorem ret_seqRight {α} (x : TimeM T α) (y : Unit → TimeM T β) [Add T] : + (SeqRight.seqRight x y).ret = (y ()).ret := rfl +@[simp] theorem ret_seqLeft {α} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : + (SeqLeft.seqLeft x y).ret = x.ret := rfl +@[simp] theorem ret_seq {α β} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) : + (Seq.seq f x).ret = f.ret (x ()).ret := rfl + +@[simp, grind =] theorem time_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) : + (m >>= f).time = m.time + (f m.ret).time := rfl +@[simp, grind =] theorem time_pure {α} [Zero T] (a : α) : (pure a : TimeM T α).time = 0 := rfl +@[simp, grind =] theorem time_map {α β} (f : α → β) (x : TimeM T α) : (f <$> x).time = x.time := rfl +@[simp] theorem time_seqRight {α} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : + (SeqRight.seqRight x y).time = x.time + (y ()).time := rfl +@[simp] theorem time_seqLeft {α} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) : + (SeqLeft.seqLeft x y).time = x.time + (y ()).time := rfl +@[simp] theorem time_seq {α β} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) : + (Seq.seq f x).time = f.time + (x ()).time := rfl + +/-- `TimeM` is lawful so long as addition in the cost is associative and absorbs zero. -/ +instance [AddMonoid T] : LawfulMonad (TimeM T) := .mk' (id_map := fun x => rfl) (pure_bind := fun _ _ => by ext <;> simp) - (bind_assoc := fun _ _ _ => by ext <;> simp [Nat.add_assoc]) + (bind_assoc := fun _ _ _ => by ext <;> simp [add_assoc]) + (seqLeft_eq := fun _ _ => by ext <;> simp) + (bind_pure_comp := fun _ _ => by ext <;> simp) -/-- Creates a `TimeM` computation with a time cost. -The time cost defaults to 1 if not provided. -/ -def tick (c : ℕ := 1) : TimeM PUnit := ⟨.unit, c⟩ +/-- Creates a `TimeM` computation with a time cost. -/ +def tick (c : T) : TimeM T PUnit := ⟨.unit, c⟩ @[simp, grind =] theorem ret_tick (c : ℕ) : (tick c).ret = () := rfl @[simp, grind =] theorem time_tick (c : ℕ) : (tick c).time = c := rfl diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean new file mode 100644 index 00000000..3cc0737f --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +namespace Turing + +variable {k : ℕ} + +namespace Routines + +@[simp] +lemma succ_iter {k r : ℕ} {i : Fin k.succ} {tapes : Fin k.succ → List (List OneTwo)} : + (Part.bind · (succ i).eval_list)^[r] (.some tapes) = Part.some (Function.update tapes i ( + if r ≠ 0 then + (dya ((dya_inv ((tapes i).headD [])) + r)) :: (tapes i).tail + else + tapes i)) := by + induction r with + | zero => simp + | succ r ih => + rw [Function.iterate_succ_apply'] + simp [ih] + grind + +--- Add 0 and 1 and store the result in 2. +--- Assumes zero for an empty tape. +def add₀ : MultiTapeTM 6 (WithSep OneTwo) := + (copy 1 2) <;> loop (h_i := by decide) 0 (succ 2) + +@[simp, grind =] +theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : + add₀.eval_list tapes = .some + (Function.update tapes 2 ((dya (dya_inv ((tapes 0).headD []) + + dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by + simp [add₀] + by_cases h : dya_inv ((tapes 0).head?.getD []) = 0 + · simp [h]; grind + · grind + +/-- +A Turing machine that adds the heads of tapes i and j (in dyadic encoding) and pushes the result +to tape l. +Assumes zero for an empty tape. -/ +public def add (i j l : Fin (k + 6)) (aux : Fin (k + 6) := ⟨k + 3, by omega⟩) + (h_inj : [i, j, l, aux, aux + 1, aux + 2].get.Injective := by decide) : + MultiTapeTM (k + 6) (WithSep OneTwo) := + add₀.with_tapes [i, j, l, aux, aux + 1, aux + 2].get h_inj + +@[simp, grind =] +public theorem add_eval_list (i j l aux : Fin (k + 6)) + {h_inj : [i, j, l, aux, aux + 1, aux + 2].get.Injective} + {tapes : Fin (k + 6) → List (List OneTwo)} : + (add i j l aux h_inj).eval_list tapes = + .some (Function.update tapes l ( + (dya (dya_inv ((tapes i).headD []) + dya_inv ((tapes j).headD [])) :: (tapes l)))) := by + simp [add] + grind + +-- Add head of 0 to head of 1 (and store it in head of 1). +def add_assign₀ : MultiTapeTM 6 (WithSep OneTwo) := + add 0 1 2 (h_inj := by decide) <;> pop 1 <;> copy 2 1 <;> pop 2 + +@[simp] +lemma add_assign₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : + add_assign₀.eval_list tapes = .some + (Function.update tapes 1 ((dya (dya_inv ((tapes 0).headD []) + + dya_inv ((tapes 1).headD [])) :: (tapes 1).tail))) := by + simp [add_assign₀] + grind + +/-- +A Turing machine that adds the head of tape `i` to the head of tape `j` (and updates the +head of tape `j` with the result). -/ +public def add_assign + (i j : Fin (k + 6)) + (aux : Fin (k + 6) := ⟨k + 2, by omega⟩) + (h_inj : [i, j, aux, aux + 1, aux + 2, aux + 3].get.Injective := by decide) : + MultiTapeTM (k + 6) (WithSep OneTwo) := + add_assign₀.with_tapes [i, j, aux, aux + 1, aux + 2, aux + 3].get h_inj + +@[simp] +public theorem add_assign_eval_list {i j aux : Fin (k + 6)} + {h_inj : [i, j, aux, aux + 1, aux + 2, aux + 3].get.Injective} + {tapes : Fin (k + 6) → List (List OneTwo)} : + (add_assign i j aux h_inj).eval_list tapes = + .some (Function.update tapes j ( + (dya (dya_inv ((tapes i).headD []) + + dya_inv ((tapes j).headD [])) :: (tapes j).tail))) := by + simpa [add_assign] using apply_updates_function_update h_inj + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean new file mode 100644 index 00000000..5d1f0464 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean @@ -0,0 +1,376 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Pim Spelier, Daan van Gent +-/ + +module + +public import Cslib.Foundations.Data.BiTape +public import Cslib.Foundations.Data.RelatesInSteps + +-- TODO create a "common file" +public import Cslib.Computability.Machines.SingleTapeTuring.Basic + +public import Mathlib.Data.Nat.PartENat +import Mathlib.Algebra.Order.BigOperators.Group.Finset + +@[expose] public section + +/-! +# Multi-Tape Turing Machines + +Defines Turing machines with `k` tapes (bidirectionally infinite, `BiTape`) containing symbols +from `Option α` for a finite alphabet `α` (where `none` is the blank symbol). + +## Important Declarations + +We define a number of structures related to Turing machine computation: + +* `Stmt`: the write and movement operations a TM can do in a single step. +* `SingleTapeTM`: the TM itself. +* `Cfg`: the configuration of a TM, including internal and tape state. +* `TimeComputable f`: a TM for computing `f`, packaged with a bound on runtime. +* `PolyTimeComputable f`: `TimeComputable f` packaged with a polynomial bound on runtime. + +We also provide ways of constructing polynomial-runtime TMs + +* `PolyTimeComputable.id`: computes the identity function +* `PolyTimeComputable.comp`: computes the composition of polynomial time machines + +## TODOs + + +-/ + +open Cslib Relation + +namespace Turing + +open BiTape StackTape + +variable {α : Type} + +variable {k : ℕ} + +/-- +A `k`-tape Turing machine +over the alphabet of `Option α` (where `none` is the blank `BiTape` symbol). +-/ +structure MultiTapeTM k α where + /-- Inhabited instance for the alphabet -/ + [αInhabited : Inhabited α] + /-- Finiteness of the alphabet -/ + [αFintype : Fintype α] + /-- type of state labels -/ + (Λ : Type) + /-- finiteness of the state type -/ + [ΛFintype : Fintype Λ] + /-- Initial state -/ + (q₀ : Λ) + /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, + and optionally the new state to transition to afterwards (`none` for halt) -/ + (M : Λ → (Fin k → Option α) → ((Fin k → (SingleTapeTM.Stmt α)) × Option Λ)) + +namespace MultiTapeTM + +section Cfg + +/-! +## Configurations of a Turing Machine + +This section defines the configurations of a Turing machine, +the step function that lets the machine transition from one configuration to the next, +and the intended initial and final configurations. +-/ + +variable (tm : MultiTapeTM k α) + +instance : Inhabited tm.Λ := ⟨tm.q₀⟩ + +instance : Fintype tm.Λ := tm.ΛFintype + +instance inhabitedStmt : Inhabited (SingleTapeTM.Stmt α) := inferInstance + +/-- +The configurations of a Turing machine consist of: +an `Option`al state (or none for the halting state), +and a `BiTape` representing the tape contents. +-/ +structure Cfg : Type where + /-- the state of the TM (or none for the halting state) -/ + state : Option tm.Λ + /-- the BiTape contents -/ + tapes : Fin k → BiTape α +deriving Inhabited + +/-- The step function corresponding to a `MultiTapeTM`. -/ +def step : tm.Cfg → Option tm.Cfg + | ⟨none, _⟩ => + -- If in the halting state, there is no next configuration + none + | ⟨some q, tapes⟩ => + -- If in state q', perform look up in the transition function + match tm.M q (fun i => (tapes i).head) with + -- and enter a new configuration with state q'' (or none for halting) + -- and tape updated according to the Stmt + | ⟨stmts, q'⟩ => some ⟨q', fun i => + ((tapes i).write (stmts i).symbol).optionMove (stmts i).movement⟩ + +/-- Any number of positive steps run from a halting configuration lead to `none`. -/ +@[simp, scoped grind =] +lemma step_iter_none_eq_none (tapes : Fin k → BiTape α) (n : ℕ) : + (Option.bind · tm.step)^[n + 1] (some ⟨none, tapes⟩) = none := by + rw [Function.iterate_succ_apply] + induction n with + | zero => simp [step] + | succ n ih => + simp only [Function.iterate_succ_apply', ih] + simp [step] + +/-- A collection of tapes where the first tape (if it exists) +contains `s` -/ +def first_tape (s : List α) : Fin k → BiTape α + | ⟨0, _⟩ => BiTape.mk₁ s + | ⟨_, _⟩ => default + +/-- +The initial configuration corresponding to a list in the input alphabet. +Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values. +This is to ensure that distinct lists map to distinct initial configurations. +-/ +@[simp, grind =] +def initCfg (s : List α) : tm.Cfg := + ⟨some tm.q₀, first_tape s⟩ + +/-- Create an initial configuration given a tuple of tapes. -/ +@[simp, grind =] +def initCfgTapes (tapes : Fin k → BiTape α) : tm.Cfg := + ⟨some tm.q₀, tapes⟩ + +/-- The final configuration corresponding to a list in the output alphabet. +(We demand that the head halts at the leftmost position of the output.) +-/ +@[simp, grind =] +def haltCfg (s : List α) : tm.Cfg := + ⟨none, first_tape s⟩ + +/-- The final configuration of a Turing machine given a sequence of tapes. -/ +@[simp, grind =] +def haltCfgTapes (tapes : Fin k → BiTape α) : tm.Cfg := + ⟨none, tapes⟩ + +/-- The configuration of the Turing machine starting with initial state and given tapes +at step `t`. -/ +def configurations (tapes : Fin k → BiTape α) (t : ℕ) : Option tm.Cfg := + (Option.bind · tm.step)^[t] (tm.initCfgTapes tapes) + +/-- +The space used by a configuration is the space used by its tape. +-/ +def Cfg.space_used (cfg : tm.Cfg) : ℕ := ∑ i, (cfg.tapes i).space_used + +lemma Cfg.space_used_step {tm : MultiTapeTM k α} (cfg cfg' : tm.Cfg) + (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + k := by + obtain ⟨_ | q, tapes⟩ := cfg + · simp [step] at hstep + · simp only [step] at hstep + generalize hM : tm.M q (fun i => (tapes i).head) = result at hstep + obtain ⟨stmts, q''⟩ := result + injection hstep with hstep + subst hstep + simp only [space_used] + trans ∑ i : Fin k, ((tapes i).space_used + 1) + · refine Finset.sum_le_sum fun i _ => ?_ + unfold BiTape.optionMove + grind [BiTape.space_used_write, BiTape.space_used_move] + · simp [Finset.sum_add_distrib] + +end Cfg + +open Cfg + +/-- +The `TransitionRelation` corresponding to a `MultiTapeTM k α` +is defined by the `step` function, +which maps a configuration to its next configuration, if it exists. +-/ +@[scoped grind =] +def TransitionRelation (tm : MultiTapeTM k α) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ + +/-- The Turing machine `tm` transforms tapes `tapes` to `tapes'` in exactly `t` steps. -/ +def TransformsTapesInTime + (tm : MultiTapeTM k α) + (tapes tapes' : Fin k → BiTape α) + (t : ℕ) : Prop := + RelatesInSteps tm.TransitionRelation ⟨some tm.q₀, tapes⟩ ⟨none, tapes'⟩ t + +/-- A proof that the Turing machine `tm` uses at most space `s` when run for up to `t` steps +on initial tapes `tapes`. -/ +def UsesSpaceUpToStep + (tm : MultiTapeTM k α) + (tapes : Fin k → BiTape α) + (s : ℕ) + (t : ℕ) : Prop := + ∀ t' ≤ t, match tm.configurations tapes t' with + | none => true + | some cfg => cfg.space_used ≤ s + +/-- The Turing machine `tm` transforms tapes `tapes` to `tapes'` in `t` steps and uses at most +`s` space. -/ +def TransformsTapesInTimeAndSpace + (tm : MultiTapeTM k α) + (tapes tapes' : Fin k → BiTape α) + (t : ℕ) (s : ℕ) : Prop := + tm.TransformsTapesInTime tapes tapes' t ∧ + tm.UsesSpaceUpToStep tapes s t + +/-- The Turing machine `tm` transforms tapes `tapes` to `tapes'` in `t` steps. -/ +def TransformsTapesWithinTime + (tm : MultiTapeTM k α) + (tapes tapes' : Fin k → BiTape α) + (t : ℕ) : Prop := + RelatesWithinSteps tm.TransitionRelation ⟨some tm.q₀, tapes⟩ ⟨none, tapes'⟩ t + +/-- The Turing machine `tm` transforms tapes `tapes` to `tapes'`. -/ +def TransformsTapes + (tm : MultiTapeTM k α) + (tapes tapes' : Fin k → BiTape α) : Prop := + ∃ t, tm.TransformsTapesInTime tapes tapes' t + +/-- The Turing machine `tm` eventually halts starting from any initial tape configuration. -/ +def haltsOn (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : Prop := + ∃ tapes', tm.TransformsTapes tapes tapes' + +@[scoped grind =] +lemma relatesInSteps_iff_step_iter_eq_some + (tm : MultiTapeTM k α) + (cfg₁ cfg₂ : tm.Cfg) + (t : ℕ) : + RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ + (Option.bind · tm.step)^[t] cfg₁ = .some cfg₂ := by + induction t generalizing cfg₁ cfg₂ with + | zero => simp + | succ t ih => + rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] + constructor + · grind only [TransitionRelation, = Option.bind_some] + · intro h_configs + cases h : (Option.bind · tm.step)^[t] cfg₁ + · grind + · rename_i cfg' + use cfg' + grind + +/-- If a Turing machine transforms tapes to tapes₁, then tapes₁ is uniquely determined. -/ +lemma transformsTapes_unique (tm : MultiTapeTM k α) + (tapes tapes₁ tapes₂ : Fin k → BiTape α) + (h1 : tm.TransformsTapes tapes tapes₁) + (h2 : tm.TransformsTapes tapes tapes₂) : + tapes₁ = tapes₂ := by + obtain ⟨t1, ht1⟩ := h1 + obtain ⟨t2, ht2⟩ := h2 + unfold TransformsTapesInTime at ht1 ht2 + rw [relatesInSteps_iff_step_iter_eq_some] at ht1 ht2 + rcases Nat.lt_trichotomy t1 t2 with hlt | heq | hgt + · -- `t1 < t2` is a contradiction because if we halt at `t1` steps + -- we cannot compute "some" after `t2` steps + obtain ⟨t', ht2_eq⟩ := Nat.exists_eq_add_of_lt hlt + rw [ht2_eq] at ht2 + rw [show t1 + t' + 1 = (t' + 1) + t1 by omega] at ht2 + rw [Function.iterate_add_apply] at ht2 + grind + · rw [heq] at ht1 + subst heq + simp_all only [step, Option.some.injEq, Cfg.mk.injEq, true_and] + · -- Symmetric to the case `t1 < t2` + obtain ⟨t', ht1_eq⟩ := Nat.exists_eq_add_of_lt hgt + rw [ht1_eq] at ht1 + rw [show t2 + t' + 1 = (t' + 1) + t2 by omega] at ht1 + rw [Function.iterate_add_apply] at ht1 + grind + +-- TODO we can actually make it computable, but we have to go a different route +-- via iterated steps +/-- +Execute the Turing machine `tm` on initial tapes `tapes`. -/ +public noncomputable def eval (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : + Part (Fin k → BiTape α) := + ⟨∃ tapes', tm.TransformsTapes tapes tapes', fun h => h.choose⟩ + +/-- +Execute the Turing machine `tm` on initial tapes `tapes` given a proof that it always halts +and thus this yields a total function. -/ +public noncomputable def eval_tot (tm : MultiTapeTM k α) {h : ∀ tapes, tm.haltsOn tapes} + (tapes : Fin k → BiTape α) : Fin k → BiTape α := + (tm.eval tapes).get (h tapes) + +-- TODO use MultiTapeTM.configurations? +-- TODO this is a simple consequence of relatesInSteps_iff_configurations_eq_some, maybe not needed. +lemma configurations_of_transformsTapesInTime + (tm : MultiTapeTM k α) + (tapes tapes' : Fin k → BiTape α) + (t : ℕ) + (h_transforms : tm.TransformsTapesInTime tapes tapes' t) : + (Option.bind · tm.step)^[t] (tm.initCfgTapes tapes) = + some (tm.haltCfgTapes tapes') := by + simp [TransformsTapesInTime] at h_transforms + apply (relatesInSteps_iff_step_iter_eq_some tm (tm.initCfgTapes tapes) ⟨none, tapes'⟩ t).mp + simpa using h_transforms + +-- TODO use MultiTapeTM.configurations? +@[scoped grind =] +lemma eval_iff_exists_steps_iter_eq_some + {tm : MultiTapeTM k α} + {tapes tapes' : Fin k → BiTape α} : + tm.eval tapes = .some tapes' ↔ + ∃ t : ℕ, (Option.bind · tm.step)^[t] (tm.initCfgTapes tapes) = + some (tm.haltCfgTapes tapes') := by + simp only [Part.eq_some_iff, eval] + constructor + · intro h + obtain ⟨h_dom, h_get⟩ := h + simp only at h_get + rw [← h_get] + obtain ⟨t, h_transforms_in_time⟩ := (h_dom.choose_spec : TransformsTapes tm tapes h_dom.choose) + use t + rw [← relatesInSteps_iff_step_iter_eq_some] + simpa [TransformsTapesInTime, initCfgTapes, haltCfgTapes] using h_transforms_in_time + · intro ⟨t, h_iter⟩ + have h_dom : ∃ tapes', tm.TransformsTapes tapes tapes' := by + use tapes' + use t + simp only [TransformsTapesInTime] + rw [relatesInSteps_iff_step_iter_eq_some] + exact h_iter + refine ⟨h_dom, ?_⟩ + apply transformsTapes_unique tm tapes + · exact (h_dom.choose_spec : TransformsTapes tm tapes h_dom.choose) + · use t + simpa [TransformsTapesInTime, relatesInSteps_iff_step_iter_eq_some] using h_iter + +/-- A proof of `tm` outputting `l'` on input `l`. -/ +def Outputs (tm : MultiTapeTM k α) (l l' : List α) : Prop := + ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') + +/-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/ +def OutputsWithinTime (tm : MultiTapeTM k α) (l l' : List α) (m : ℕ) := + RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m + +-- /-- +-- This lemma bounds the size blow-up of the output of a Turing machine. +-- It states that the increase in length of the output over the input is bounded by the runtime. +-- This is important for guaranteeing that composition of polynomial time Turing machines +-- remains polynomial time, as the input to the second machine +-- is bounded by the output length of the first machine. +-- -/ +-- lemma output_length_le_input_length_add_time (tm : MultiTapeTM k α) (l l' : List α) (t : ℕ) +-- (h : tm.OutputsWithinTime l l' t) : +-- l'.length ≤ max 1 l.length + k * t := by +-- obtain ⟨steps, hsteps_le, hevals⟩ := h +-- grind [hevals.apply_le_apply_add (Cfg.space_used tm) +-- fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)] + +end MultiTapeTM + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean new file mode 100644 index 00000000..96a71504 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] + +def copy₁ : MultiTapeTM 2 (WithSep α) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +lemma copy₁_eval_list {tapes : Fin 2 → List (List α)} : + copy₁.eval_list tapes = + Part.some (Function.update tapes 1 (((tapes 0).headD []) :: tapes 1)) := by + sorry + +/-- +A Turing machine that copies the first word on tape `i` to tape `j`. +If Tape `i` is empty, pushes the empty word to tape `j`. +-/ +public def copy {k : ℕ} (i j : ℕ) + (h_neq : i ≠ j := by decide) + (h_i_lt : i < k := by decide) + (h_j_lt : j < k := by decide) : + MultiTapeTM k (WithSep α) := + copy₁.with_tapes [⟨i, h_i_lt⟩, ⟨j, h_j_lt⟩].get (by intro x y; grind) + +@[simp, grind =] +public lemma copy_eval_list + {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k} + {tapes : Fin k → List (List α)} : + (copy i j (h_neq := h_neq) (h_i_lt) (h_j_lt)).eval_list tapes = Part.some + (Function.update tapes ⟨j, h_j_lt⟩ + (((tapes ⟨i, h_i_lt⟩).headD []) :: (tapes ⟨j, h_j_lt⟩))) := by + have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind + simp_all [copy] + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean new file mode 100644 index 00000000..7ad2b42c --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +import Mathlib.Logic.Function.Basic + +namespace Turing + +namespace Routines + +/-- +A 3-tape Turing machine that pushes the new word "1" +to the third tape if the first words on the first and second tape are the same +and otherwise pushes the empty word to the third tape. +If one of the first two tapes is empty, uses the empty word for comparison. +-/ +def eq₀ : MultiTapeTM 3 (WithSep OneTwo) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +theorem eq₀_eval_list {tapes : Fin 3 → List (List OneTwo)} : + eq₀.eval_list tapes = + Part.some (Function.update tapes 2 ((if (tapes 0).headD [] = (tapes 1).headD [] then + [.one] + else + []) :: (tapes 2))) := by + sorry + +/-- +A Turing machine that pushes the new word "1" +to tape `t` if the first words on tape `q` and tape `s` are the same +and otherwise pushes the empty word to tape `t`. +If one of the tapes `q` or `s` are empty, uses the empty word for comparison. +-/ +public def eq {k : ℕ} (q s t : Fin k) + (h_inj : [q, s, t].get.Injective := by intro x y; grind) : + MultiTapeTM k (WithSep OneTwo) := + eq₀.with_tapes [q, s, t].get h_inj + +@[grind =] +public theorem eq_eval_list {k : ℕ} {q s t : Fin k} + (h_inj : [q, s, t].get.Injective) + {tapes : Fin k → List (List OneTwo)} : + (eq q s t).eval_list tapes = + Part.some (Function.update tapes t ((if (tapes q).headD [] = (tapes s).headD [] then + [.one] + else + []) :: (tapes t))) := by + simp [eq] + grind + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean new file mode 100644 index 00000000..508491ca --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +import Cslib.Foundations.Data.BiTape +import Cslib.Foundations.Data.RelatesInSteps + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats + +-- TODO create a "common file" +import Cslib.Computability.Machines.SingleTapeTuring.Basic + +namespace Turing + + +-- This is an attempt at proving Savitch's theorem. We start by stating a generic +-- space-efficient graph reachability algorithm. + +/- + +General idea, assume distance is power of two: + +def reachable(a, b, t, r): + if t = 0: + return r(a, b) + else: + for c in vertices: + if reachable(a, c, t - 1, r) and reachable(c, b, t - 1, r): + return True + return False + +Until we have a generic mechanism for recursion, let's translate this into a program that +uses "goto", and every variable is a stack: + +def reachable(a, b, t, r): + terminate = 0 + result = 0 + section = [0] + while !terminate: + match section.pop() + | 0 => + if t = 0: + result = r(a, b) + terminate = 1 + section.push(7) + else: + section.push(1) + | 1 => + c.push(0) + section.push(2) + | 2 => + if c.top() = num_vertices: + section.push(6) + else: + a.push(a.top()) + b.push(c.top()) + section.push(0) + t.push(t.top() - 1) + section.push(3) + | 3 => + section.push(4) + + + +-/ + + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean new file mode 100644 index 00000000..d0ea26b2 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/HeadStats.lean @@ -0,0 +1,69 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension + +-- TODO create a "common file" +import Cslib.Computability.Machines.SingleTapeTuring.Basic + +namespace Turing + +variable [Inhabited α] + +variable {k : ℕ} + +/-- Statistics on the tape head movements. -/ +public structure HeadStats where + /-- The minimal (left-most) position of the head during the computation, + relative to the starting position. -/ + min : ℤ + /-- The maximal (right-most) position of the head during the computation, + relative to the starting position. -/ + max : ℤ + /-- The final position of the head after the computation, relative to the + starting position. -/ + final : ℤ + h_bounds : min ≤ final ∧ final ≤ max ∧ min ≤ 0 ∧ 0 ≤ max + +/-- The space required. -/ +public def HeadStats.space (hs : HeadStats) : ℕ := + (1 + hs.max - hs.min).toNat -- TODO we know it is nonnegative, is there a way to make use of that? + + +/-- Compute the head statistics for a turing machine starting with a certain tape configuration. -/ +public def headStats (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : + Part (Fin k → HeadStats) := sorry + +/-- Execute a Turing machine and also compute head statistics. -/ +public def MultiTapeTM.evalWithStats (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : + Part ((Fin k → BiTape α) × (Fin k → HeadStats)) := sorry + +-- move this somewhere else +def seq (tm₁ tm₂ : MultiTapeTM k α) : MultiTapeTM k α := sorry + +def seq_combine_stats (stats₁ stats₂ : Fin k → HeadStats) : Fin k → HeadStats := + fun i => match (stats₁ i, stats₂ i) with + | (⟨min₁, max₁, final₁, h₁⟩, ⟨min₂, max₂, final₂, h₂⟩) => + ⟨min min₁ (min₂ + final₁), + max max₁ (max₂ + final₁), + final₁ + final₂, + by omega⟩ + +lemma seq_evalWithStats (tm₁ tm₂ : MultiTapeTM k α) (tapes : Fin k → BiTape α) (i : Fin k) : + (seq tm₁ tm₂).evalWithStats tapes = do + let (tapes', stats₁) ← tm₁.evalWithStats tapes + let (tapes'', stats₂) ← tm₂.evalWithStats tapes' + return (tapes'', seq_combine_stats stats₁ stats₂) := by sorry + +-- Next step: relate space requirements and head stats. + +theorem stats_and_space (tm : MultiTapeTM k α) (tapes tapes' : Fin k → BiTape α) (s : ℕ) : + (∃ t, tm.TransformsTapesInTimeAndSpace tapes tapes' t s) ↔ + ∃ hs, (∑ i, (hs i).space) ≤ s ∧ tm.evalWithStats tapes = .some (tapes', hs) := by sorry +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean new file mode 100644 index 00000000..fcd35f7b --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/IsZeroRoutine.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.IteCombinator + +namespace Turing + +variable {k : ℕ} + +namespace Routines + +/-- +A Turing machine that computes the logical negation: It replaces an empty (or non-existing) head +on tape `i` by the word "1" and everything else by the empty word. -/ +public def isZero (i : Fin k) := ite i (pop i <;> push i []) (pop i <;> push i [OneTwo.one]) + +@[simp, grind =] +public theorem isZero_eval_list {i : Fin k} {tapes : Fin k → List (List OneTwo)} : + (isZero i).eval_list tapes = .some (Function.update tapes i ( + (if (tapes i).headD [] = [] then [OneTwo.one] else []) :: (tapes i).tail)) := by + simp [isZero] + grind + +end Routines +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean new file mode 100644 index 00000000..e0bf71b8 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/IteCombinator.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] +variable {k : ℕ} + +/-- +A Turing machine combinator that runs `tm₁` if the first word on tape `i` exists and is non-empty, +otherwise it runs `tm₂`. -/ +public def ite (i : Fin k) (tm₁ tm₂ : MultiTapeTM k (WithSep α)) : + MultiTapeTM k (WithSep α) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp, grind =] +public theorem ite_eval_list + {i : Fin k} + {tm₁ tm₂ : MultiTapeTM k (WithSep α)} + {tapes : Fin k → List (List α)} : + (ite i tm₁ tm₂).eval_list tapes = + if (tapes i).headD [] = [] then tm₂.eval_list tapes else tm₁.eval_list tapes := by + sorry + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean new file mode 100644 index 00000000..7e44e4d3 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -0,0 +1,179 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +import Mathlib.Tactic.DeriveFintype + +namespace Turing + +/-- +An alphabet that contains exactly two symbols, 1 and 2. +TODO use an embedding or something else that is more flexible +-/ +public inductive OneTwo where + | one + | two +deriving DecidableEq, Inhabited, Fintype + + +/-- An alphabet for list encoding -/ +public inductive WithSep (α : Type) where + | blank + | ofChar (c : α) + | comma + -- TODO need to decide if we want to encode lists with parentheses or not. + -- Is annoying when pushing and popping from lists, but can be useful to avoid + -- running "off the tape" + -- | lParen + -- | rParen +deriving Fintype, DecidableEq, Inhabited + +/-- A list of words is transformed by appending a comma after each word and concatenating. +Note that the comma is not only a separator but also appears as the final character +of the resulting string (if the list is non-empty). -/ +public def listToString (ls : List (List α)) : List (WithSep α) := + (ls.map (fun w : List α => (w.map .ofChar) ++ [.comma])).flatten + +/-- Encodes a list of words into a tape. -/ +public def listToTape (ls : List (List α)) : BiTape (WithSep α) := + BiTape.mk₁ (listToString ls) + +/-- The Turing machine `tm` transforms the list-encoded tapes `tapes` into the list-encoded +tapes `tapes'`. -/ +public def MultiTapeTM.TransformsLists + (tm : MultiTapeTM k (WithSep α)) + (tapes tapes' : Fin k → List (List α)) : Prop := + tm.TransformsTapes (listToTape ∘ tapes) (listToTape ∘ tapes') + +/-- The Turing machine `tm` halts starting with list-encoded tapes `tapes`. -/ +public def MultiTapeTM.HaltsOnLists + (tm : MultiTapeTM k (WithSep α)) + (tapes : Fin k → List (List α)) : Prop := + ∃ tapes', tm.TransformsLists tapes tapes' + +/-- Execute the Turing machine `tm` on the list-encoded tapes `tapes`. -/ +public noncomputable def MultiTapeTM.eval_list + (tm : MultiTapeTM k (WithSep α)) + (tapes : Fin k → List (List α)) : + Part (Fin k → List (List α)) := + ⟨tm.HaltsOnLists tapes, fun h => h.choose⟩ + +public theorem MultiTapeTM.HaltsOnLists_of_eval_list + {tm : MultiTapeTM k (WithSep α)} + {tapes : Fin k → List (List α)} + (h_dom : (tm.eval_list tapes).Dom) : + tm.HaltsOnLists tapes := by + simpa using h_dom + +/-- Execute the Turing machine `tm` knowing that it always halts, thus yielding a total function +on the tapes. -/ +public noncomputable def MultiTapeTM.eval_list_tot + (tm : MultiTapeTM k (WithSep α)) + (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes) + (tapes : Fin k → List (List α)) : + Fin k → List (List α) := + (tm.eval_list tapes).get (h_alwaysHalts tapes) + +@[simp, grind =] +public theorem MultiTapeTM.extend_eval_list + {α : Type} [Fintype α] + {k₁ k₂ : ℕ} {h_le : k₁ ≤ k₂} + {tm : MultiTapeTM k₁ (WithSep α)} + {tapes : Fin k₂ → List (List α)} : + (tm.extend h_le).eval_list tapes = + (tm.eval_list (tapes ⟨·, by omega⟩)).map (fun tapes' => + fun i : Fin k₂ => if h : i.val < k₁ then tapes' ⟨i, h⟩ else tapes i) := by + sorry + +@[simp, grind =] +public theorem MultiTapeTM.permute_tapes_eval_list + {α : Type} [Fintype α] [Inhabited α] + (tm : MultiTapeTM k (WithSep α)) (σ : Equiv.Perm (Fin k)) (tapes : Fin k → List (List α)) : + (tm.permute_tapes σ).eval_list tapes = + (tm.eval_list (tapes ∘ σ)).map (fun tapes' => tapes' ∘ σ.symm) := by + sorry + +@[simp, grind =] +public theorem MultiTapeTM.with_tapes_eval_list + {α : Type} [Fintype α] [Inhabited α] + {k₁ k₂ : ℕ} + {tm : MultiTapeTM k₁ (WithSep α)} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective} + {tapes : Fin k₂ → List (List α)} : + (tm.with_tapes f h_inj).eval_list tapes = + (tm.eval_list (tapes ∘ f)).map + (fun tapes' => fun t => apply_updates tapes tapes' f t) := by + sorry + +def MultiTapeTM.TransformsListsWithStats + (tm : MultiTapeTM k (WithSep α)) + (tapes : Fin k → List (List α)) + (ts : (Fin k → List (List α)) × (Fin k → HeadStats)) : Prop := + tm.evalWithStats (listToTape ∘ tapes) = .some (listToTape ∘ ts.1, ts.2) + +/-- +Evaluate the Turing machine `tm` on the list-encoded tapes `tapes` and also return the head +statistics of the computation. +-/ +public noncomputable def MultiTapeTM.evalWithStats_list + (tm : MultiTapeTM k (WithSep α)) + (tapes : Fin k → List (List α)) : + Part ((Fin k → List (List α)) × (Fin k → HeadStats)) := + ⟨∃ ts, tm.TransformsListsWithStats tapes ts, fun h => h.choose⟩ + +-- TODO for machines running on lists, we can actually have more precise head stats: +-- we know (and should enforce) that the head never moves to the right of the rightmost symbol +-- and always starts and ends on the leftmost symbol (and if the tape is empty, it never moves +-- to the right of the starting position). +-- So the minimal information we need is (per tape) the amount of symbols that were used beyond +-- the max of the ones in the initial and final configuration. +-- TODO it also makes sense to allow upper bounds on that. + +/-- +The Turing machine `tm` computes a total function on lists and this uniquely +determined function is `f`. +-/ +public def MultiTapeTM.computes + (tm : MultiTapeTM k (WithSep α)) + (f : (Fin k → List (List α)) → (Fin k → List (List α))) : Prop := + ∀ tapes, tm.eval_list tapes = .some (f tapes) + +public theorem MultiTapeTM.eval_of_computes + {tm : MultiTapeTM k (WithSep α)} + {f : (Fin k → List (List α)) → (Fin k → List (List α))} + (h_computes : tm.computes f) + {tapes : Fin k → List (List α)} : + tm.eval_list tapes = .some (f tapes) := by + specialize h_computes tapes + simpa [MultiTapeTM.computes] using h_computes + + +/-- Dyadic encoding of natural numbers. -/ +public def dya (n : ℕ) : List OneTwo := + if n = 0 then [] + else if Even n then + dya (n / 2 - 1) ++ [.two] + else + dya ((n - 1) / 2) ++ [.one] + +/-- Dyadic decoding of natural numbers. -/ +public def dya_inv : List OneTwo → ℕ := sorry + +@[simp, grind =] +public lemma dya_inv_zero : dya_inv [] = 0 := by + sorry + +@[simp, grind =] +public lemma dya_inv_dya (n : ℕ) : dya_inv (dya n) = n := by sorry + +@[simp, grind =] +public lemma dya_dya_inv (w : List OneTwo) : dya (dya_inv w) = w := by sorry + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean new file mode 100644 index 00000000..c4cf18f0 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/LoopCombinator.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding + +namespace Turing + +namespace Routines + +variable {k : ℕ} + +/-- +A Turing machine that executes `tm` a number of times as given by the first word on tape `i`. +If tape `i` is empty, do not execute the TM. +Note that the iteration counter is not directly available to `tm`. -/ +public def loop (i : ℕ) {h_i : i < k} + (tm : MultiTapeTM k (WithSep OneTwo)) : MultiTapeTM (k + 3) (WithSep OneTwo) := + sorry + -- let target : Fin (k + (aux + 3)) := ⟨aux, by omega⟩ + -- let counter : Fin (k + (aux + 3)) := ⟨aux + 1, by omega⟩ + -- let cond : Fin (k + (aux + 3)) := ⟨aux + 2, by omega⟩ + -- (copy (k := k + (aux + 3)) i target (h_neq := by grind) <;> + -- push counter [] <;> + -- neq target counter cond (by grind) (by grind) (by grind) <;> + -- doWhile cond ( + -- pop cond <;> + -- tm.toMultiTapeTM <;> + -- succ counter <;> + -- neq target counter cond (by grind) (by grind) (by grind)) <;> + -- pop cond <;> + -- pop counter <;> + -- pop target).set_aux_tapes (aux + 3) + + +@[simp] +public theorem loop_eval_list {i : ℕ} {h_i : i < k} + {tm : MultiTapeTM k (WithSep OneTwo)} + {tapes : Fin (k + 3) → List (List OneTwo)} : + (loop i tm (h_i := h_i)).eval_list tapes = + (((Part.bind · tm.eval_list)^[dya_inv ((tapes ⟨i, by omega⟩).headD [])] + (Part.some (tapes_take tapes k (by omega))))).map + fun tapes' => tapes_extend_by tapes' tapes := by + sorry + +end Routines +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/MoveRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/MoveRoutine.lean new file mode 100644 index 00000000..b65d7b6e --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/MoveRoutine.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] + +/-- A 1-tape Turing machine that moves its head in a given direction +once and then halts. -/ +public def move (dir : Dir) : MultiTapeTM 1 α where + Λ := PUnit + q₀ := 0 + M _ syms := (fun i => ⟨syms i, some dir⟩, none) + +@[simp] +public lemma move_eval (tape : BiTape α) (dir : Turing.Dir) : + (move dir).eval (fun _ => tape) = .some (fun _ => tape.move dir) := by + rw [MultiTapeTM.eval_iff_exists_steps_iter_eq_some] + use 1 + rfl + +/-- A 1-tape Turing machine that moves its head in a given direction until a condition +on the read symbol is met. -/ +public def move_until (dir : Turing.Dir) (cond : (Option α) → Bool) : MultiTapeTM 1 α where + Λ := PUnit + q₀ := PUnit.unit + M q syms := match cond (syms 0) with + | false => (fun _ => ⟨syms 0, some dir⟩, some q) + | true => (fun _ => ⟨syms 0, none⟩, none) + +lemma move_until_step_cond_false + {tape : BiTape α} + {stop_condition : Option α → Bool} + (h_neg_stop : ¬ stop_condition tape.head) : + (move_until .right stop_condition).step + ⟨some (move_until .right stop_condition).q₀, (fun _ => tape)⟩ = + some ⟨some (move_until .right stop_condition).q₀, (fun _ => tape.move .right)⟩ := by + simp [move_until, h_neg_stop, BiTape.optionMove, MultiTapeTM.step] + +lemma move_until_step_cond_true + {tape : BiTape α} + {stop_condition : Option α → Bool} + (h_neg_stop : stop_condition tape.head) : + (move_until .right stop_condition).step + ⟨some (move_until .right stop_condition).q₀, (fun _ => tape)⟩ = + some ⟨none, (fun _ => tape)⟩ := by + simp [move_until, h_neg_stop, BiTape.optionMove, MultiTapeTM.step] + +public theorem move_until.right_semantics + (tape : BiTape α) + (stop_condition : Option α → Bool) + (h_stop : ∃ n : ℕ, stop_condition (tape.nth n)) : + (move_until .right stop_condition).eval (fun _ => tape) = + .some (fun _ => tape.move_int (Nat.find h_stop)) := by + rw [MultiTapeTM.eval_iff_exists_steps_iter_eq_some] + let n := Nat.find h_stop + use n.succ + have h_not_stop_of_lt : ∀ k < n, ¬ stop_condition (tape.move_int k).head := by + intro k hk + simp [Nat.find_min h_stop hk] + have h_iter : ∀ k < n, (Option.bind · (move_until .right stop_condition).step)^[k] + (some ⟨some (move_until .right stop_condition).q₀, fun _ => tape⟩) = + some ⟨some (move_until .right stop_condition).q₀, fun _ => tape.move_int k⟩ := by + intro k hk + induction k with + | zero => + simp [BiTape.move_int] + | succ k ih => + have hk' : k < n := Nat.lt_of_succ_lt hk + rw [Function.iterate_succ_apply', ih hk'] + simp only [Option.bind_some, move_until_step_cond_false (h_not_stop_of_lt k hk')] + simp [BiTape.move, ← BiTape.move_int_one_eq_move_right, BiTape.move_int_move_int] + have h_n_eq : n = Nat.find h_stop := by grind + by_cases h_n_zero : n = 0 + · have h_stop_cond : stop_condition (tape.head) := by simp_all [n] + let h_step := move_until_step_cond_true h_stop_cond + simp [h_step, ← h_n_eq, h_n_zero] + · obtain ⟨n', h_n'_eq_n_succ⟩ := Nat.exists_eq_add_one_of_ne_zero h_n_zero + rw [h_n'_eq_n_succ, Function.iterate_succ_apply', Function.iterate_succ_apply'] + have h_n'_lt_n : n' < n := by omega + simp only [MultiTapeTM.initCfgTapes, MultiTapeTM.haltCfgTapes] + rw [h_iter n' h_n'_lt_n] + simp only [Option.bind_some, move_until_step_cond_false (h_not_stop_of_lt n' h_n'_lt_n)] + simp only [BiTape.move, ← BiTape.move_int_one_eq_move_right, BiTape.move_int_move_int] + rw [show (n' : ℤ) + 1 = n by omega] + have h_n_stop : stop_condition ((tape.move_int n).head) := by + simpa [n] using Nat.find_spec h_stop + simpa using move_until_step_cond_true h_n_stop + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean new file mode 100644 index 00000000..1eee2595 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.AddRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +namespace Turing + +variable {k : ℕ} + +namespace Routines + +-- Multiplies the heads of 0 and 1 and stores the result in 2. +def mul₀ : MultiTapeTM 9 (WithSep OneTwo) := + (push 2 []) <;> loop 0 (h_i := by omega) (add_assign 1 2 3) + +@[simp] +lemma add_assign_iter {i j aux : Fin (k + 6)} {r : ℕ} + (h_inj : [i, j, aux, aux + 1, aux + 2, aux + 3].get.Injective) + {tapes : Fin (k + 6) → List (List OneTwo)} : + (Part.bind · (add_assign i j aux h_inj).eval_list)^[r] (.some tapes) = + Part.some (Function.update tapes j ( + if r = 0 then + tapes j + else + (dya ((dya_inv ((tapes j).headD [])) + r * (dya_inv ((tapes i).headD [])))) :: + (tapes j).tail)) := by + induction r with + | zero => simp + | succ r ih => + rw [Function.iterate_succ_apply'] + simp only [ih, Part.bind_some] + rw [add_assign_eval_list] + have h_neq : i ≠ j := Function.Injective.ne h_inj (a₁ := 0) (a₂ := 1) (by grind) + simp + grind + +@[simp] +theorem mul₀_eval_list {tapes : Fin 9 → List (List OneTwo)} : + mul₀.eval_list tapes = .some + (Function.update tapes 2 ( + (dya (dya_inv ((tapes 0).headD []) * dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by + by_cases h_zero: dya_inv ((tapes 0).head?.getD []) = 0 + · simp [mul₀, h_zero] + grind + · simp [mul₀, h_zero] + grind + +/-- +A Turing machine that multiplies the heads of tapes i and j and pushes the result to tape l. +If tapes are empty, their heads are assumed to be zero. +-/ +public def mul + (i j l : Fin (k + 9)) + (aux : Fin (k + 9) := ⟨k + 3, by omega⟩) + (h_inj : [i, j, l, aux, aux + 1, aux + 2, aux + 3, aux + 4, aux + 5].get.Injective := by decide) : + MultiTapeTM (k + 9) (WithSep OneTwo) := + mul₀.with_tapes [i, j, l, aux, aux + 1, aux + 2, aux + 3, aux + 4, aux + 5].get h_inj + +@[simp, grind =] +public theorem mul_eval_list (i j l aux : Fin (k + 9)) + {h_inj : [i, j, l, aux, aux + 1, aux + 2, aux + 3, aux + 4, aux + 5].get.Injective} + {tapes : Fin (k + 9) → List (List OneTwo)} : + (mul i j l aux h_inj).eval_list tapes = + .some (Function.update tapes l ( + (dya (dya_inv ((tapes i).headD []) * dya_inv ((tapes j).headD [])) :: (tapes l)))) := by + simpa [mul] using apply_updates_function_update h_inj + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean new file mode 100644 index 00000000..7b615a0d --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/PopRoutine.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] + +def pop₁ : MultiTapeTM 1 (WithSep α) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +lemma pop₁_eval_list {tapes : Fin 1 → List (List α)} : + pop₁.eval_list tapes = .some (Function.update tapes 0 (tapes 0).tail) := by + sorry + +/-- +A Turing machine that removes the first word on tape `i`. If the tape is empty, does nothing. +-/ +public def pop {k : ℕ} (i : Fin k) : MultiTapeTM k (WithSep α) := + pop₁.with_tapes [i].get (by intro x y; grind) + +@[simp, grind =] +public theorem pop_eval_list {k : ℕ} {i : Fin k} + {tapes : Fin k → List (List α)} : + (pop i).eval_list tapes = .some (Function.update tapes i (tapes i).tail) := by + have h_inj : [i].get.Injective := by intro x y; grind + simp_all [pop] + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean new file mode 100644 index 00000000..c703a1e4 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/PushRoutine.lean @@ -0,0 +1,45 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] + +def push₁ (w : List α) : MultiTapeTM 1 (WithSep α) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +lemma push₁_eval_list {w : List α} {tapes : Fin 1 → List (List α)} : + (push₁ w).eval_list tapes = .some (Function.update tapes 0 (w :: (tapes 0))) := by + sorry + +/-- +A Turing machine that pushes the word `w` to tape `i`. +-/ +public def push {k : ℕ} (i : Fin k) (w : List α) : MultiTapeTM k (WithSep α) := + (push₁ w).with_tapes [i].get (by intro x y; grind) + +@[simp, grind =] +public theorem push_eval_list {k : ℕ} + {i : Fin k} {w : List α} {tapes : Fin k → List (List α)} : + (push i w).eval_list tapes = + .some (Function.update tapes i (w :: (tapes i))) := by + have h_inj : [i].get.Injective := by intro x y; grind + simp_all [push] + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean new file mode 100644 index 00000000..dba01653 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/SequentialCombinator.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +import Cslib.Foundations.Data.BiTape +import Cslib.Foundations.Data.RelatesInSteps + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding + +namespace Turing + +namespace MultiTapeTM + +variable [Inhabited α] +variable {k : ℕ} + +/-- +Sequential combination of Turing machines. Runs `tm₁` and then `tm₂` on the resulting tapes +(if the first one halts). +-/ +public def seq (tm₁ tm₂ : MultiTapeTM k α) : MultiTapeTM k α := sorry + +public theorem seq_eval + (tm₁ tm₂ : MultiTapeTM k α) + (tapes₀ : Fin k → BiTape α) : + (seq tm₁ tm₂).eval tapes₀ = + tm₁.eval tapes₀ >>= fun tape₁ => tm₂.eval tape₁ := by + sorry + +@[simp, grind =] +public theorem seq_eval_list + {tm₁ tm₂ : MultiTapeTM k (WithSep α)} + {tapes₀ : Fin k → List (List α)} : + (seq tm₁ tm₂).eval_list tapes₀ = + tm₁.eval_list tapes₀ >>= fun tape₁ => tm₂.eval_list tape₁ := by + sorry + +public theorem seq_associative + (tm₁ tm₂ tm₃ : MultiTapeTM k α) + (tapes₀ : Fin k → List (List α)) : + (seq (seq tm₁ tm₂) tm₃).eval = (seq tm₁ (seq tm₂ tm₃)).eval := by + sorry + +/-- +Sequential combination of Turing machines. +-/ +infixl:90 " <;> " => seq + + +end MultiTapeTM + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean new file mode 100644 index 00000000..8c4f6bb9 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean @@ -0,0 +1,59 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +import Cslib.Foundations.Data.BiTape +import Cslib.Foundations.Data.RelatesInSteps + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes + +import Mathlib.Data.Nat.Bits + +namespace Turing + +namespace Routines + +def succ₀ : MultiTapeTM 1 (WithSep OneTwo) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +lemma succ₀_eval_list {tapes : Fin 1 → List (List OneTwo)} : + succ₀.eval_list tapes = .some (Function.update tapes 0 + ((dya (dya_inv ((tapes 0).headD [])).succ) :: (tapes 0).tail)) := by + sorry + +/-- +A Turing machine that increments the head of tape `i` by one (in dyadic encoding). +Pushes zero if the tape is empty. -/ +public def succ {k : ℕ} (i : Fin k) : MultiTapeTM k (WithSep OneTwo) := + succ₀.with_tapes [i].get (by intro x y; grind) + +@[simp] +public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} : + (succ i).eval_list tapes = .some (Function.update tapes i + ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail)) := by + simpa [succ] using apply_updates_function_update (by intro x y; grind) + +lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} : + succ₀.evalWithStats_list [(dya n) :: ls].get = + .some ( + [(dya n.succ) :: ls].get, + -- this depends on if we have overflow on the highest dyadic character or not. + if (dya n.succ).length = (dya n).length then + [⟨0, (dya n).length, 0, by omega⟩].get + else + [⟨-1, (dya n).length, -1, by omega⟩].get) := by + sorry + + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean b/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean new file mode 100644 index 00000000..43c6e9ca --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean @@ -0,0 +1,74 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +import Cslib.Foundations.Data.BiTape +import Cslib.Foundations.Data.RelatesInSteps + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic + +namespace Turing + +variable [Inhabited α] [Fintype α] + +/-- Extend a Turing machine to work with more tapes. +The added tapes are not acted upon. -/ +public def MultiTapeTM.extend {k₁ k₂ : ℕ} (h_le : k₁ ≤ k₂) + (tm : MultiTapeTM k₁ α) : MultiTapeTM k₂ α where + Λ := tm.Λ + q₀ := tm.q₀ + M := fun q syms => match tm.M q (fun i => syms ⟨i, by omega⟩) with + | (stmts, q') => + (fun i => if h : i < k₁ then stmts ⟨i, h⟩ else default, q') + +/-- +Restrict a sequence of tapes to the first `k'` tapes. +-/ +@[simp] +public abbrev tapes_take + {γ : Type} + (tapes : Fin k → γ) + (k' : ℕ) + (h_le : k' ≤ k) + (i : Fin k') : γ := + tapes ⟨i, by omega⟩ + +@[simp] +public lemma Function.update_tapes_take + {γ : Type} + (k : ℕ) + {k' : ℕ} + {h_le : k' ≤ k} + {tapes : Fin k → γ} + {p : Fin k'} + {v : γ} : + Function.update (tapes_take tapes k' h_le) p v = + tapes_take (Function.update tapes ⟨p, by omega⟩ v) k' h_le := by + sorry + +/-- +Extend a sequence of tapes by adding more tapes at the end. +Ignores the first `k₁` tapes of `extend_by` and uses the rest. +-/ +@[simp] +public abbrev tapes_extend_by + {γ : Type} + {k₁ k₂ : ℕ} + (tapes : Fin k₁ → γ) + (extend_by : Fin k₂ → γ) + (i : Fin k₂) : γ := + if h : i < k₁ then tapes ⟨i, h⟩ else extend_by i + +@[simp, grind =] +public lemma MultiTapeTM.extend_eval {k₁ k₂ : ℕ} (h_le : k₁ ≤ k₂) + (tm : MultiTapeTM k₁ α) + {tapes : Fin k₂ → BiTape α} : + (tm.extend h_le).eval tapes = + (tm.eval (tapes ⟨·, by omega⟩)).map (fun tapes' => tapes_extend_by tapes' tapes) := by + sorry + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean new file mode 100644 index 00000000..dbc78721 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +import Cslib.Foundations.Data.BiTape +import Cslib.Foundations.Data.RelatesInSteps + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] +variable {k : ℕ} + +/-- +Repeatedly run a sub routine as long as a condition on the symbol +at the head of tape `i` is true. +-/ +public def doWhileSymbol (cond : Option α → Bool) (i : Fin k) (tm : MultiTapeTM k α) : + MultiTapeTM k α where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +public theorem doWhileSymbol_eval + (cond : Option α → Bool) + (i : Fin k) + (tm : MultiTapeTM k α) + (tapes_seq : ℕ → Fin k → BiTape α) + (h_transform : ∀ j, tm.eval (tapes_seq j) = .some (tapes_seq j.succ)) + (h_stops : ∃ m, cond (tapes_seq m i).head = false) : + (doWhileSymbol cond i tm).eval (tapes_seq 0) = .some (tapes_seq (Nat.find h_stops)) := by + sorry + +/-- Repeatedly run a sub routine as long as the first word on tape `i` is non-empty. +-/ +public def doWhile (i : Fin k) (tm : MultiTapeTM k (WithSep α)) : + MultiTapeTM k (WithSep α) where + Λ := PUnit + q₀ := 0 + M _ syms := sorry + +@[simp] +public theorem doWhile_eval_list + {i : Fin k} + {tm : MultiTapeTM k (WithSep α)} + {tapes : Fin k → List (List α)} + (h_halts : ∀ tapes', tm.HaltsOnLists tapes') : + (doWhile i tm).eval_list tapes = + ⟨∃ n, ((tm.eval_list_tot h_halts)^[n] tapes i).head?.getD [] = [], + fun h_loopEnds => (tm.eval_list_tot h_halts)^[Nat.find h_loopEnds] tapes⟩ := by + sorry + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean new file mode 100644 index 00000000..a4d97db5 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/WithTapes.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension + +public import Mathlib.Logic.Equiv.Fintype +public import Mathlib.Data.Finset.Sort + +namespace Turing + +variable [Inhabited α] [Fintype α] + +variable {k : ℕ} + +/-- +Permute tapes according to a bijection. +-/ +public def MultiTapeTM.permute_tapes + (tm : MultiTapeTM k α) (σ : Equiv.Perm (Fin k)) : MultiTapeTM k α where + Λ := tm.Λ + q₀ := tm.q₀ + M := fun q syms => match tm.M q (syms ∘ σ) with + | (stmts, q') => (stmts ∘ σ.symm, q') + +--- General theorem: permuting tapes commutes with evaluation +@[simp, grind =] +public theorem MultiTapeTM.permute_tapes_eval + (tm : MultiTapeTM k α) (σ : Equiv.Perm (Fin k)) (tapes : Fin k → BiTape α) : + (tm.permute_tapes σ).eval tapes = + (tm.eval (tapes ∘ σ)).map (fun tapes' => tapes' ∘ σ.symm) := by + sorry + +private def findFin {k : ℕ} (p : Fin k → Prop) [DecidablePred p] (h : ∃ i, p i) : Fin k := + (Finset.univ.filter p).min' (by + simp only [Finset.Nonempty, Finset.mem_filter, Finset.mem_univ, true_and] + exact h) + +def inj_to_perm {k₁ k₂ : ℕ} (f : Fin k₁ → Fin k₂) (h_inj : f.Injective) : + Equiv.Perm (Fin k₂) + -- non-computable version + -- let f' : {i : Fin k₂ // i < k₁} → Fin k₂ := fun ⟨i, _⟩ => f ⟨i, by omega⟩ + -- have h_f'_inj : f'.Injective := by intro a b h; grind + -- (Equiv.ofInjective f' h_f'_inj).extendSubtype + where + toFun := sorry + invFun := sorry + left_inv := by sorry + right_inv := by sorry + +/-- +Change the order of the tapes of a Turing machine. +Example: For a 2-tape Turing machine tm, +`tm.with_tapes [2, 4].get (by grind)` is a 5-tape Turing machine whose tape 2 is +the original machine's tape 0 and whose tape 4 is the original +machine's tape 1 +Note that `f` is a function to `Fin k₂`, which means that integer literals +automatically wrap. You have to be careful to make sure that the target machine +has the right amount of tapes. +-/ +public def MultiTapeTM.with_tapes {k₁ k₂ : ℕ} +-- TODO use embedding instead? + (tm : MultiTapeTM k₁ α) (f : Fin k₁ → Fin k₂) (h_inj : f.Injective) : MultiTapeTM k₂ α := + (tm.extend + (by simpa using Fintype.card_le_of_injective f h_inj)).permute_tapes (inj_to_perm f h_inj) + +-- TODO do not use `h.choose` here but rather assume that `f` is injective. + +/-- +Updates `tapes` by choosing elements from `tapes'` according to (the partial inverse of) `f`. +-/ +public noncomputable def apply_updates + {γ : Type} + {k₁ k₂ : ℕ} + (tapes : Fin k₂ → γ) + (tapes' : Fin k₁ → γ) + (f : Fin k₁ → Fin k₂) + (i : Fin k₂) : γ := + if h : ∃ j, f j = i then tapes' h.choose else tapes i + +@[simp, grind =] +public lemma apply_updates_function_update_apply + {γ : Type} + {k₁ k₂ : ℕ} + {tapes : Fin k₂ → γ} + {f : Fin k₁ → Fin k₂} + (h_inj : f.Injective) + {t : Fin k₁} + {new_val : γ} + {i : Fin k₂} : + apply_updates tapes (Function.update (tapes ∘ f) t new_val) f i = + Function.update tapes (f t) new_val i := by + sorry + +@[simp, grind =] +public lemma apply_updates_function_update + {γ : Type} + {k₁ k₂ : ℕ} + {tapes : Fin k₂ → γ} + {f : Fin k₁ → Fin k₂} + (h_inj : f.Injective) + {t : Fin k₁} + {new_val : γ} : + apply_updates tapes (Function.update (tapes ∘ f) t new_val) f = + Function.update tapes (f t) new_val := by + funext i + apply apply_updates_function_update_apply h_inj + +@[simp, grind =] +public theorem MultiTapeTM.with_tapes_eval + {k₁ k₂ : ℕ} + {tm : MultiTapeTM k₁ α} {f : Fin k₁ → Fin k₂} {h_inj : f.Injective} + {tapes : Fin k₂ → BiTape α} : + (tm.with_tapes f h_inj).eval tapes = + (tm.eval (tapes ∘ f)).map + (fun tapes' => fun t => apply_updates tapes tapes' f t) := by + simp [with_tapes] + sorry + + +end Turing diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean new file mode 100644 index 00000000..10e291cd --- /dev/null +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -0,0 +1,490 @@ +/- +Copyright (c) 2026 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Pim Spelier, Daan van Gent +-/ + +module + +public import Cslib.Foundations.Data.BiTape +public import Cslib.Foundations.Data.RelatesInSteps +public import Mathlib.Algebra.Polynomial.Eval.Defs + +@[expose] public section + +/-! +# Single-Tape Turing Machines + +Defines a single-tape Turing machine for computing functions on `List α` for finite alphabet `α`. +These machines have access to a single bidirectionally-infinite tape (`BiTape`) +which uses symbols from `Option α`. + +## Important Declarations + +We define a number of structures related to Turing machine computation: + +* `Stmt`: the write and movement operations a TM can do in a single step. +* `SingleTapeTM`: the TM itself. +* `Cfg`: the configuration of a TM, including internal and tape state. +* `TimeComputable f`: a TM for computing `f`, packaged with a bound on runtime. +* `PolyTimeComputable f`: `TimeComputable f` packaged with a polynomial bound on runtime. + +We also provide ways of constructing polynomial-runtime TMs + +* `PolyTimeComputable.id`: computes the identity function +* `PolyTimeComputable.comp`: computes the composition of polynomial time machines + +## TODOs + +- Encoding of types in lists to represent computations on arbitrary types. +- Add `∘` notation for `compComputer`. + +-/ + +open Cslib Relation + +namespace Turing + +open BiTape StackTape + +variable {α : Type} + +namespace SingleTapeTM + +/-- +A Turing machine "statement" is just a `Option`al command to move left or right, +and write a symbol (i.e. an `Option α`, where `none` is the blank symbol) on the `BiTape` +-/ +structure Stmt (α : Type) where + /-- The symbol to write at the current head position -/ + symbol : Option α + /-- The direction to move the tape head -/ + movement : Option Dir +deriving Inhabited + +end SingleTapeTM + +/-- +A single-tape Turing machine +over the alphabet of `Option α` (where `none` is the blank `BiTape` symbol). +-/ +structure SingleTapeTM α where + /-- Inhabited instance for the alphabet -/ + [αInhabited : Inhabited α] + /-- Finiteness of the alphabet -/ + [αFintype : Fintype α] + /-- type of state labels -/ + (Λ : Type) + /-- finiteness of the state type -/ + [ΛFintype : Fintype Λ] + /-- Initial state -/ + (q₀ : Λ) + /-- Transition function, mapping a state and a head symbol to a `Stmt` to invoke, + and optionally the new state to transition to afterwards (`none` for halt) -/ + (M : Λ → Option α → SingleTapeTM.Stmt α × Option Λ) + +namespace SingleTapeTM + +section Cfg + +/-! +## Configurations of a Turing Machine + +This section defines the configurations of a Turing machine, +the step function that lets the machine transition from one configuration to the next, +and the intended initial and final configurations. +-/ + +variable (tm : SingleTapeTM α) + +instance : Inhabited tm.Λ := ⟨tm.q₀⟩ + +instance : Fintype tm.Λ := tm.ΛFintype + +instance inhabitedStmt : Inhabited (Stmt α) := inferInstance + +/-- +The configurations of a Turing machine consist of: +an `Option`al state (or none for the halting state), +and a `BiTape` representing the tape contents. +-/ +structure Cfg : Type where + /-- the state of the TM (or none for the halting state) -/ + state : Option tm.Λ + /-- the BiTape contents -/ + BiTape : BiTape α +deriving Inhabited + +/-- The step function corresponding to a `SingleTapeTM`. -/ +@[simp] +def step : tm.Cfg → Option tm.Cfg + | ⟨none, _⟩ => + -- If in the halting state, there is no next configuration + none + | ⟨some q', t⟩ => + -- If in state q', perform look up in the transition function + match tm.M q' t.head with + -- and enter a new configuration with state q'' (or none for halting) + -- and tape updated according to the Stmt + | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩ + +/-- +The initial configuration corresponding to a list in the input alphabet. +Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values. +This is to ensure that distinct lists map to distinct initial configurations. +-/ +def initCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩ + +/-- The final configuration corresponding to a list in the output alphabet. +(We demand that the head halts at the leftmost position of the output.) +-/ +def haltCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩ + +/-- +The space used by a configuration is the space used by its tape. +-/ +def Cfg.space_used (tm : SingleTapeTM α) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used + +@[scoped grind =] +lemma Cfg.space_used_initCfg (tm : SingleTapeTM α) (s : List α) : + (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s + +@[scoped grind =] +lemma Cfg.space_used_haltCfg (tm : SingleTapeTM α) (s : List α) : + (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s + +lemma Cfg.space_used_step {tm : SingleTapeTM α} (cfg cfg' : tm.Cfg) + (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by + obtain ⟨_ | q, tape⟩ := cfg + · simp [step] at hstep + · simp only [step] at hstep + generalize hM : tm.M q tape.head = result at hstep + obtain ⟨⟨wr, dir⟩, q''⟩ := result + cases hstep; cases dir with + | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] + | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using + BiTape.space_used_move (tape.write wr) d + +end Cfg + +open Cfg + +/-- +The `TransitionRelation` corresponding to a `SingleTapeTM α` +is defined by the `step` function, +which maps a configuration to its next configuration, if it exists. +-/ +@[scoped grind =] +def TransitionRelation (tm : SingleTapeTM α) (c₁ c₂ : tm.Cfg) : Prop := tm.step c₁ = some c₂ + +/-- A proof of `tm` outputting `l'` on input `l`. -/ +def Outputs (tm : SingleTapeTM α) (l l' : List α) : Prop := + ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l') + +/-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/ +def OutputsWithinTime (tm : SingleTapeTM α) (l l' : List α) (m : ℕ) := + RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m + +/-- +This lemma bounds the size blow-up of the output of a Turing machine. +It states that the increase in length of the output over the input is bounded by the runtime. +This is important for guaranteeing that composition of polynomial time Turing machines +remains polynomial time, as the input to the second machine +is bounded by the output length of the first machine. +-/ +lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ) + (h : tm.OutputsWithinTime l l' t) : + l'.length ≤ max 1 l.length + t := by + obtain ⟨steps, hsteps_le, hevals⟩ := h + grind [hevals.apply_le_apply_add (Cfg.space_used tm) + fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)] + +section Computers + +variable [Inhabited α] [Fintype α] + +/-- A Turing machine computing the identity. -/ +def idComputer : SingleTapeTM α where + Λ := PUnit + q₀ := PUnit.unit + M _ b := ⟨⟨b, none⟩, none⟩ + +/-- +A Turing machine computing the composition of two other Turing machines. + +If f and g are computed by Turing machines `tm1` and `tm2` +then we can construct a Turing machine which computes g ∘ f by first running `tm1` +and then, when `tm1` halts, transitioning to the start state of `tm2` and running `tm2`. +-/ +def compComputer (tm1 tm2 : SingleTapeTM α) : SingleTapeTM α where + -- The states of the composed machine are the disjoint union of the states of the input machines. + Λ := tm1.Λ ⊕ tm2.Λ + -- The start state is the start state of the first input machine. + q₀ := .inl tm1.q₀ + M q h := + match q with + -- If we are in the first input machine's states, run that machine ... + | .inl ql => match tm1.M ql h with + | (stmt, state) => + -- ... taking the same tape action as the first input machine would. + (stmt, + match state with + -- If it halts, transition to the start state of the second input machine + | none => some (.inr tm2.q₀) + -- Otherwise continue as normal + | _ => Option.map .inl state) + -- If we are in the second input machine's states, run that machine ... + | .inr qr => + match tm2.M qr h with + | (stmt, state) => + -- ... taking the same tape action as the second input machine would. + (stmt, + match state with + -- If it halts, transition to the halting state + | none => none + -- Otherwise continue as normal + | _ => Option.map .inr state) + +section compComputerLemmas + +/-! ### Composition Computer Lemmas -/ + +variable (tm1 tm2 : SingleTapeTM α) (cfg1 : tm1.Cfg) (cfg2 : tm2.Cfg) + +lemma compComputer_q₀_eq : (compComputer tm1 tm2).q₀ = Sum.inl tm1.q₀ := rfl + +/-- +Convert a `Cfg` over the first input machine to a config over the composed machine. +Note it may transition to the start state of the second machine if the first machine halts. +-/ +private def toCompCfg_left : (compComputer tm1 tm2).Cfg := + match cfg1.state with + | some q => ⟨some (Sum.inl q), cfg1.BiTape⟩ + | none => ⟨some (Sum.inr tm2.q₀), cfg1.BiTape⟩ + +/-- Convert a `Cfg` over the second input machine to a config over the composed machine -/ +private def toCompCfg_right : (compComputer tm1 tm2).Cfg := + ⟨Option.map Sum.inr cfg2.state, cfg2.BiTape⟩ + +/-- The initial configuration for the composed machine, with the first machine starting. -/ +private def initialCfg (input : List α) : (compComputer tm1 tm2).Cfg := + ⟨some (Sum.inl tm1.q₀), BiTape.mk₁ input⟩ + +/-- The intermediate configuration for the composed machine, +after the first machine halts and the second machine starts. -/ +private def intermediateCfg (intermediate : List α) : (compComputer tm1 tm2).Cfg := + ⟨some (Sum.inr tm2.q₀), BiTape.mk₁ intermediate⟩ + +/-- The final configuration for the composed machine, after the second machine halts. -/ +private def finalCfg (output : List α) : (compComputer tm1 tm2).Cfg := + ⟨none, BiTape.mk₁ output⟩ + +/-- The left converting function commutes with steps of the machines. -/ +private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) : + Option.map (toCompCfg_left tm1 tm2) (tm1.step cfg1) = + (compComputer tm1 tm2).step (toCompCfg_left tm1 tm2 cfg1) := by + cases cfg1 with | mk state BiTape => cases state with + | none => grind + | some q => + simp only [step, toCompCfg_left, compComputer] + -- generalize hM : tm1.M q BiTape.head = result + -- obtain ⟨⟨wr, dir⟩, nextState⟩ := result + grind [toCompCfg_left, compComputer, step] + +/-- The right converting function commutes with steps of the machines. -/ +private theorem map_toCompCfg_right_step : + Option.map (toCompCfg_right tm1 tm2) (tm2.step cfg2) = + (compComputer tm1 tm2).step (toCompCfg_right tm1 tm2 cfg2) := by + cases cfg2 with + | mk state BiTape => + cases state with + | none => + simp only [step, toCompCfg_right, Option.map_none, compComputer] + | some q => + generalize hM : tm2.M q BiTape.head = result + obtain ⟨⟨wr, dir⟩, nextState⟩ := result + simp only [compComputer] + grind [toCompCfg_right, step, compComputer] + +/-- +Simulation for the first phase of the composed computer. +When the first machine runs from start to halt, the composed machine +runs from start (with Sum.inl state) to Sum.inr tm2.q₀ (the start of the second phase). +This takes the same number of steps because the halt transition becomes a transition to the +second machine. +-/ +private theorem comp_left_relatesWithinSteps (input intermediate : List α) (t : ℕ) + (htm1 : + RelatesWithinSteps tm1.TransitionRelation + (tm1.initCfg input) + (tm1.haltCfg intermediate) + t) : + RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation + (initialCfg tm1 tm2 input) + (intermediateCfg tm1 tm2 intermediate) + t := by + simp only [initialCfg, intermediateCfg, initCfg, haltCfg] at htm1 ⊢ + refine RelatesWithinSteps.map (toCompCfg_left tm1 tm2) ?_ htm1 + intro a b hab + have ha : a.state.isSome := by + simp only [TransitionRelation, step] at hab + cases a with | mk state _ => cases state <;> simp_all + have h1 := map_toCompCfg_left_step tm1 tm2 a ha + rw [hab, Option.map_some] at h1 + exact h1.symm + +/-- +Simulation for the second phase of the composed computer. +When the second machine runs from start to halt, the composed machine +runs from Sum.inr tm2.q₀ to halt. +-/ +private theorem comp_right_relatesWithinSteps (intermediate output : List α) (t : ℕ) + (htm2 : + RelatesWithinSteps tm2.TransitionRelation + (tm2.initCfg intermediate) + (tm2.haltCfg output) + t) : + RelatesWithinSteps (compComputer tm1 tm2).TransitionRelation + (intermediateCfg tm1 tm2 intermediate) + (finalCfg tm1 tm2 output) + t := by + simp only [intermediateCfg, finalCfg, initCfg, haltCfg] at htm2 ⊢ + refine RelatesWithinSteps.map (toCompCfg_right tm1 tm2) ?_ htm2 + intro a b hab + grind [map_toCompCfg_right_step tm1 tm2 a] + +end compComputerLemmas + +end Computers + +/-! +## Time Computability + +This section defines the notion of time-bounded Turing Machines +-/ + +section TimeComputable + +variable [Inhabited α] [Fintype α] + +/-- A Turing machine + a time function + +a proof it outputs `f` in at most `time(input.length)` steps. -/ +structure TimeComputable (f : List α → List α) where + /-- the underlying bundled SingleTapeTM -/ + tm : SingleTapeTM α + /-- a bound on runtime -/ + time_bound : ℕ → ℕ + /-- proof this machine outputs `f` in at most `time_bound(input.length)` steps -/ + outputsFunInTime (a) : tm.OutputsWithinTime a (f a) (time_bound a.length) + + +/-- The identity map on α is computable in constant time. -/ +def TimeComputable.id : TimeComputable (α := α) id where + tm := idComputer + time_bound _ := 1 + outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩ + +/-- +Time bounds for `compComputer`. + +The `compComputer` of two machines which have time bounds is bounded by + +* The time taken by the first machine on the input size +* added to the time taken by the second machine on the output size of the first machine + (which is itself bounded by the time taken by the first machine) + +Note that we require the time function of the second machine to be monotone; +this is to ensure that if the first machine returns an output +which is shorter than the maximum possible length of output for that input size, +then the time bound for the second machine still holds for that shorter input to the second machine. +-/ +def TimeComputable.comp {f g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) + (h_mono : Monotone hg.time_bound) : + (TimeComputable (g ∘ f)) where + tm := compComputer hf.tm hg.tm + -- perhaps it would be good to track the blow up separately? + time_bound l := (hf.time_bound l) + hg.time_bound (max 1 l + hf.time_bound l) + outputsFunInTime a := by + have hf_outputsFun := hf.outputsFunInTime a + have hg_outputsFun := hg.outputsFunInTime (f a) + simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, + haltCfg] at hg_outputsFun hf_outputsFun ⊢ + -- The computer reduces a to f a in time hf.time_bound a.length + have h_a_reducesTo_f_a : + RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation + (initialCfg hf.tm hg.tm a) + (intermediateCfg hf.tm hg.tm (f a)) + (hf.time_bound a.length) := + comp_left_relatesWithinSteps hf.tm hg.tm a (f a) + (hf.time_bound a.length) hf_outputsFun + -- The computer reduces f a to g (f a) in time hg.time_bound (f a).length + have h_f_a_reducesTo_g_f_a : + RelatesWithinSteps (compComputer hf.tm hg.tm).TransitionRelation + (intermediateCfg hf.tm hg.tm (f a)) + (finalCfg hf.tm hg.tm (g (f a))) + (hg.time_bound (f a).length) := + comp_right_relatesWithinSteps hf.tm hg.tm (f a) (g (f a)) + (hg.time_bound (f a).length) hg_outputsFun + -- Therefore, the computer reduces a to g (f a) in the sum of those times. + have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a + apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a + refine Nat.add_le_add_left ?_ (hf.time_bound a.length) + · apply h_mono + -- Use the lemma about output length being bounded by input length + time + exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a) + +end TimeComputable + +/-! +## Polynomial Time Computability + +This section defines polynomial time computable functions on Turing machines, +and proves that: + +* The identity function is polynomial time computable +* The composition of two polynomial time computable functions is polynomial time computable + +-/ + +section PolyTimeComputable + +open Polynomial + +variable [Inhabited α] [Fintype α] + +/-- A Turing machine + a polynomial time function + +a proof it outputs `f` in at most `time(input.length)` steps. -/ +structure PolyTimeComputable (f : List α → List α) extends TimeComputable f where + /-- a polynomial time bound -/ + poly : Polynomial ℕ + /-- proof that this machine outputs `f` in at most `time(input.length)` steps -/ + bounds : ∀ n, time_bound n ≤ poly.eval n + +/-- A proof that the identity map on α is computable in polytime. -/ +noncomputable def PolyTimeComputable.id : @PolyTimeComputable (α := α) id where + toTimeComputable := TimeComputable.id + poly := 1 + bounds _ := by simp [TimeComputable.id] + +-- TODO remove `h_mono` assumption +-- by developing function to convert PolyTimeComputable into one with monotone time bound +/-- +A proof that the composition of two polytime computable functions is polytime computable. +-/ +noncomputable def PolyTimeComputable.comp {f g : List α → List α} + (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) + (h_mono : Monotone hg.time_bound) : + PolyTimeComputable (g ∘ f) where + toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono + poly := hf.poly + hg.poly.comp (1 + X + hf.poly) + bounds n := by + simp only [TimeComputable.comp, eval_add, eval_comp, eval_X, eval_one] + apply add_le_add + · exact hf.bounds n + · exact (h_mono (add_le_add (by omega) (hf.bounds n))).trans (hg.bounds _) + +end PolyTimeComputable + +end SingleTapeTM + +end Turing diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean new file mode 100644 index 00000000..e8ef4809 --- /dev/null +++ b/Cslib/Foundations/Data/BiTape.lean @@ -0,0 +1,274 @@ +/- +Copyright (c) 2026 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Christian Reitwiessner +-/ + +module + +public import Cslib.Foundations.Data.StackTape +public import Mathlib.Computability.TuringMachine + +@[expose] public section + +/-! +# BiTape: Bidirectionally infinite TM tape representation using StackTape + +This file defines `BiTape`, a tape representation for Turing machines +in the form of an `List` of `Option` values, +with the additional property that the list cannot end with `none`. + +## Design + +Note that Mathlib has a `Tape` type, but it requires the alphabet type to be inhabited, +and considers the ends of the tape to be filled with default values. + +This design requires the tape elements to be `Option` values, and ensures that +`List`s of the base alphabet, rendered directly onto the tape by mapping over `some`, +will not collide. + +## Main definitions + +* `BiTape`: A tape with a head symbol and left/right contents stored as `StackTape` +* `BiTape.move`: Move the tape head left or right +* `BiTape.write`: Write a symbol at the current head position +* `BiTape.space_used`: The space used by the tape +-/ + +namespace Turing + +/-- +A structure for bidirectionally-infinite Turing machine tapes +that eventually take on blank `none` values +-/ +structure BiTape (α : Type) where + /-- The symbol currently under the tape head -/ + head : Option α + /-- The contents to the left of the head -/ + left : StackTape α + /-- The contents to the right of the head -/ + right : StackTape α + +namespace BiTape + +/-- The empty `BiTape` -/ +def nil {α} : BiTape α := ⟨none, ∅, ∅⟩ + +instance {α : Type} : Inhabited (BiTape α) where + default := nil + +instance {α : Type} : EmptyCollection (BiTape α) := + ⟨nil⟩ + +@[simp] +lemma empty_eq_nil {α} : (∅ : BiTape α) = nil := rfl + +/-- +Given a `List` of `α`, construct a `BiTape` by mapping the list to `some` elements +and laying them out to the right side, +with the head under the first element of the list if it exists. +-/ +def mk₁ {α} (l : List α) : BiTape α := + match l with + | [] => ∅ + | h :: t => { head := some h, left := ∅, right := StackTape.map_some t } + +/-- Indexes the tape using integers, where `0` is the symbol at the tape head, +positive integers index to the right, and negative integers index to the left. -/ +def nth {α} (t : BiTape α) (n : ℤ) : Option α := + match n with + | Int.ofNat 0 => t.head + | Int.ofNat (n + 1) => t.right.toList.getD n none + | Int.negSucc n => t.left.toList.getD n none + +@[simp, grind =] +lemma nth_zero {α} (t : BiTape α) : + t.nth 0 = t.head := by rfl + +lemma ext_nth {α} {t₁ t₂ : BiTape α} (h_nth_eq : ∀ n, t₁.nth n = t₂.nth n) : + t₁ = t₂ := by + cases t₁ with | mk head₁ left₁ right₁ + cases t₂ with | mk head₂ left₂ right₂ + simp only [mk.injEq] + refine ⟨?_, ?_, ?_⟩ + · -- head₁ = head₂ + have := h_nth_eq 0 + simpa [nth] using this + · -- left₁ = left₂ + apply StackTape.ext_toList + intro n + have := h_nth_eq (Int.negSucc n) + sorry -- simpa [nth] using this + + · -- right₁ = right₂ + apply StackTape.ext_toList + intro n + have := h_nth_eq (Int.ofNat (n + 1)) + sorry -- simpa [nth] using this + +section Move + +/-- +Move the head left by shifting the left StackTape under the head. +-/ +def move_left {α} (t : BiTape α) : BiTape α := + ⟨t.left.head, t.left.tail, StackTape.cons t.head t.right⟩ + +/-- +Move the head right by shifting the right StackTape under the head. +-/ +def move_right {α} (t : BiTape α) : BiTape α := + ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩ + +/-- +Move the head to the left or right, shifting the tape underneath it. +-/ +def move {α} (t : BiTape α) : Dir → BiTape α + | .left => t.move_left + | .right => t.move_right + +/-- +Optionally perform a `move`, or do nothing if `none`. +-/ +def optionMove {α} : BiTape α → Option Dir → BiTape α + | t, none => t + | t, some d => t.move d + +@[simp] +lemma move_left_move_right {α} (t : BiTape α) : t.move_left.move_right = t := by + simp [move_right, move_left] + +@[simp] +lemma move_right_move_left {α} (t : BiTape α) : t.move_right.move_left = t := by + simp [move_left, move_right] + + +@[simp, grind =] +lemma move_right_nth {α} (t : BiTape α) (p : ℤ) : + (t.move_right).nth p = t.nth (p + 1) := by + unfold nth + split + · grind [move_right] + · rename_i n + simp only [move_right, List.getD_eq_getElem?_getD, Nat.succ_eq_add_one, Int.ofNat_eq_natCast, + Int.natCast_add, Int.cast_ofNat_Int] + have h: (n : ℤ) + 1 + 1 ≥ 2 := by omega + split + · grind + · rename_i n'' h_eq + simp at h_eq + rw [show n'' = n + 1 by omega] + simp + · grind + · rename_i n + simp only [move_right, List.getD_eq_getElem?_getD] + split + · rename_i h_eq + simp only [StackTape.cons] + grind + · grind + · rename_i n' h_eq + rw [show n = n' + 1 by omega] + simp only [StackTape.cons] + grind + +@[simp, grind =] +lemma move_left_nth {α} (t : BiTape α) (p : ℤ) : + (t.move_left).nth p = t.nth (p - 1) := by + rw [← move_left_move_right t] + simp only [move_right_nth] + simp + +@[simp, grind =] +lemma move_right_iter_nth {α} (t : BiTape α) (n : ℕ) (p : ℤ) : + (move_right^[n] t).nth p = t.nth (p + n) := by + induction n generalizing p with + | zero => simp + | succ n ih => + simp only [Function.iterate_succ_apply'] + grind + +@[simp, grind =] +lemma move_left_iter_nth {α} (t : BiTape α) (n : ℕ) (p : ℤ) : + (move_left^[n] t).nth p = t.nth (p - n) := by + induction n generalizing p with + | zero => simp + | succ n ih => + simp only [Function.iterate_succ_apply'] + grind + +/-- Move the head by an integer amount of cells where positive amounts cause the tape head to move +to the right while a negative amounts move the tape head to the left. -/ +def move_int {α} (t : BiTape α) (delta : ℤ) : BiTape α := + match delta with + | Int.ofNat n => move_right^[n] t + | Int.negSucc n => move_left^[n + 1] t + +@[simp, grind =] +lemma move_int_zero_eq_id {α} (t : BiTape α) : + t.move_int 0 = t := by rfl + +@[simp, grind =] +lemma move_int_one_eq_move_right {α} (t : BiTape α) : + t.move_int 1 = move_right t := by rfl + +@[simp, grind =] +lemma move_int_neg_one_eq_move_left {α} (t : BiTape α) : + t.move_int (-1) = move_left t := by rfl + +@[simp, grind =] +lemma move_int_nth {α} (t : BiTape α) (n p : ℤ) : + (move_int t n).nth p = t.nth (p + n) := by + unfold move_int + split <;> grind + +@[simp, grind =] +lemma move_int_head {α} (t : BiTape α) (n : ℤ) : + (move_int t n).head = t.nth n := by + simp [← nth_zero, move_int_nth] + +@[simp, grind =] +lemma move_int_move_int {α} (t : BiTape α) (n₁ n₂ : ℤ) : + (t.move_int n₁).move_int n₂ = t.move_int (n₁ + n₂) := by + apply BiTape.ext_nth + grind + +end Move + +/-- +Write a value under the head of the `BiTape`. +-/ +def write {α} (t : BiTape α) (a : Option α) : BiTape α := { t with head := a } + +@[simp, grind =] +lemma write_head {α} (t : BiTape α) : t.write t.head = t := by rfl + +/-- +The space used by a `BiTape` is the number of symbols +between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`. +-/ +@[scoped grind] +def space_used {α} (t : BiTape α) : ℕ := 1 + t.left.length + t.right.length + +@[simp, grind =] +lemma space_used_write {α} (t : BiTape α) (a : Option α) : + (t.write a).space_used = t.space_used := by rfl + +lemma space_used_mk₁ {α} (l : List α) : + (mk₁ l).space_used = max 1 l.length := by + cases l with + | nil => simp [mk₁, space_used, nil, StackTape.length_nil] + | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega + +@[simp, grind =] +lemma space_used_defaul {α} : (default : BiTape α).space_used = 1 := by + simp [space_used, nil, default] + +lemma space_used_move {α} (t : BiTape α) (d : Dir) : + (t.move d).space_used ≤ t.space_used + 1 := by + cases d <;> grind [move_left, move_right, move, + space_used, StackTape.length_tail_le, StackTape.length_cons_le] + +end BiTape + +end Turing diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean index 07c66d0f..04106f01 100644 --- a/Cslib/Foundations/Data/RelatesInSteps.lean +++ b/Cslib/Foundations/Data/RelatesInSteps.lean @@ -124,9 +124,8 @@ lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} : If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the number of steps. -/ -lemma RelatesInSteps.apply_le_apply_add {a b : α} (h : α → ℕ) - (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (m : ℕ) (hevals : RelatesInSteps r a b m) : +lemma RelatesInSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesInSteps r a b m) + (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) : h b ≤ h a + m := by induction hevals with | refl => simp @@ -200,12 +199,12 @@ lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ} /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the step bound. -/ -lemma RelatesWithinSteps.apply_le_apply_add {a b : α} (h : α → ℕ) - (h_step : ∀ a b, r a b → h b ≤ h a + 1) - (n : ℕ) (hevals : RelatesWithinSteps r a b n) : - h b ≤ h a + n := by +lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m) + (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1) + : + h b ≤ h a + m := by obtain ⟨m, hm, hevals_m⟩ := hevals - have := RelatesInSteps.apply_le_apply_add h h_step m hevals_m + have := RelatesInSteps.apply_le_apply_add hevals_m h h_step lia /-- diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean new file mode 100644 index 00000000..558570f1 --- /dev/null +++ b/Cslib/Foundations/Data/StackTape.lean @@ -0,0 +1,199 @@ +/- +Copyright (c) 2026 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ + +module + +public import Cslib.Init +public import Mathlib.Data.List.Basic + +@[expose] public section + +/-! +# StackTape: Infinite, eventually-`none` lists of `Option`s + +This file defines `StackTape`, a stack-like data structure of `Option` values, +where the tape is considered to be infinite and eventually all `none`s. +This is useful as a data structure with a simple API for manipulation by Turing machines. + +## Design + +`StackTape` is represented as a list of `Option` values where the list cannot end with `none`. +The end of the list is then treated as the start of an infinite sequence of `none` values +by the low-level API. +This design makes it convenient to express the length of the tape in terms of the list length. + +An alternative design would be to represent the tape as a `Stream' (Option α)`, +with additional fields tracking the length and the fact that the stream eventually becomes `none`. +This design might complicate reasoning about the length of the tape, but could make other operations +more straightforward. + +Future design work might explore this alternative representation and compare its +advantages and disadvantages. + +## TODO + +- Make a `::`-like notation. + +-/ + +namespace Turing + +/-- +An infinite tape representation using a list of `Option` values, +where the list is eventually `none`. + +Represented as a `List (Option α)` that does not end with `none`. +-/ +structure StackTape (α : Type) where + /-- The underlying list representation -/ + toList : List (Option α) + /-- + The list can be empty (i.e. `none`), + but if it is not empty, the last element is not (`some`) `none` + -/ + toList_getLast?_ne_some_none : toList.getLast? ≠ some none + +attribute [scoped grind! .] StackTape.toList_getLast?_ne_some_none + +namespace StackTape + +/-- The empty `StackTape` -/ +@[scoped grind] +def nil {α} : StackTape α := ⟨[], by grind⟩ + +instance {α : Type} : Inhabited (StackTape α) where + default := nil + +instance {α : Type} : EmptyCollection (StackTape α) := + ⟨nil⟩ + +@[simp] +lemma empty_eq_nil {α} : (∅ : StackTape α) = nil := rfl + +@[simp, scoped grind =] +lemma nil_toList {α} : (nil : StackTape α).toList = [] := rfl + +/-- Prepend an `Option` to the `StackTape` -/ +@[scoped grind] +def cons {α} (x : Option α) (xs : StackTape α) : StackTape α := + match x, xs with + | none, ⟨[], _⟩ => ⟨[], by grind⟩ + | none, ⟨hd :: tl, hl⟩ => ⟨none :: hd :: tl, by grind⟩ + | some a, ⟨l, hl⟩ => ⟨some a :: l, by grind⟩ + +@[simp, scoped grind =] +lemma cons_none_nil_toList {α} : (cons none (nil : StackTape α)).toList = [] := by grind + +@[simp, scoped grind =] +lemma cons_some_toList {α} (a : α) (l : StackTape α) : + (cons (some a) l).toList = some a :: l.toList := by simp only [cons] + +/-- Remove the first element of the `StackTape`, returning the rest -/ +@[scoped grind] +def tail {α} (l : StackTape α) : StackTape α := + match hl : l.toList with + | [] => nil + | hd :: t => ⟨t, by grind⟩ + +/-- Get the first element of the `StackTape`. -/ +@[scoped grind] +def head {α} (l : StackTape α) : Option α := + match l.toList with + | [] => none + | h :: _ => h + +@[grind =] +lemma head_eq_list_getD {α} (l : StackTape α) : l.head = l.toList.getD 0 none := by + cases l with | mk toList h => + cases toList <;> grind + +@[simp, scoped grind =] +lemma tail_toList_get_eq_right_toList_get_succ {α} (t : StackTape α) (n : ℕ) : + t.tail.toList[n]? = t.toList[n + 1]? := by grind + +lemma eq_iff {α} (l1 l2 : StackTape α) : l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by + constructor + · grind + · intro ⟨hhead, htail⟩ + cases l1 with | mk as1 h1 => + cases l2 with | mk as2 h2 => + cases as1 <;> cases as2 <;> grind + +@[simp] +lemma head_cons {α} (o : Option α) (l : StackTape α) : (cons o l).head = o := by + cases o with + | none => + cases l with | mk toList hl => + cases toList <;> grind + | some a => grind + +@[simp] +lemma tail_cons {α} (o : Option α) (l : StackTape α) : (cons o l).tail = l := by + cases o with + | none => + cases l with | mk toList h => + cases toList <;> grind + | some a => + simp only [cons, tail] + +@[simp] +lemma cons_head_tail {α} (l : StackTape α) : + cons (l.head) (l.tail) = l := by + rw [eq_iff] + simp + +lemma ext_toList {α} {s₁ s₂ : StackTape α} + (h : ∀ (n : ℕ), s₁.toList.getD n none = s₂.toList.getD n none) : + s₁ = s₂ := by + -- TODO not sure how to prove this. The main idea behind this type is that + -- toList is injective, so it should be true. + sorry + +lemma ext_iff {α} {s₁ s₂ : StackTape α} : + s₁ = s₂ ↔ s₁.toList = s₂.toList := by + cases s₁ with | mk l₁ h₁ => + cases s₂ with | mk l₂ h₂ => + simp + +/-- Create a `StackTape` from a list by mapping all elements to `some` -/ +@[scoped grind] +def map_some {α} (l : List α) : StackTape α := ⟨l.map some, by simp⟩ + +section Length + +/-- The length of the `StackTape` is the number of elements up to the last non-`none` element -/ +@[scoped grind] +def length {α} (l : StackTape α) : ℕ := l.toList.length + +lemma length_tail_le {α} (l : StackTape α) : l.tail.length ≤ l.length := by + grind + +grind_pattern length_tail_le => l.tail.length + +@[scoped grind =] +lemma length_cons_none {α} (l : StackTape α) : + (cons none l).length = l.length + if l.length = 0 then 0 else 1 := by + cases l with | mk toList h => + cases toList <;> grind + +@[scoped grind =] +lemma length_cons_some {α} (a : α) (l : StackTape α) : (cons (some a) l).length = l.length + 1 := by + grind + +lemma length_cons_le {α} (o : Option α) (l : StackTape α) : (cons o l).length ≤ l.length + 1 := by + cases o <;> grind + +@[simp, scoped grind =] +lemma length_map_some {α} (l : List α) : (map_some l).length = l.length := by grind + +@[simp, scoped grind =] +lemma length_nil {α} : (nil : StackTape α).length = 0 := by grind + +end Length + +end StackTape + +end Turing