Lax765601.Derivatives

Derivatives of a string-to-string function

concepts/Lax765601/Derivatives.lean · lax-765601

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

In the paper

page 29 of the paper of lax-157538, Transducers

Definition

A derivative of a length preserving string-to-string function $f : A^* \to B^*$ is a function of the form

f(w\_) \;:\; v \;\mapsto\; f(wv) \text{ with the first } |w| \text{ letters of the output removed},

for some input string $w$ (Section A.2.3 of Transducers). The derivative is the output that $f$ still produces after having read $w$ ; for a function computed by a Mealy machine it is determined by the state reached after reading $w$ , which is the observation behind the Myhill–Nerode lemma for Mealy machines (Lemma A.2.10): a function is computed by a Mealy machine if and only if it is letter-to-letter, its $n$ -th output letter depends only on the first $n$ input letters, and it has finitely many derivatives. The minimal Mealy machine of such a function has the derivatives as its states.

Lean source view on GitHub

1	import Mathlib.Data.List.Basic
2
3	/-!
4	---
5	title: Derivatives of a string-to-string function
6	type: definition
7	---
8	A derivative of a length preserving string-to-string function $f : A^* \to B^*$
9	is a function of the form
10	$f(w\_) \;:\; v \;\mapsto\; f(wv) \text{ with the first } \|w\| \text{ letters of the output removed},$
11	for some input string $w$ (Section A.2.3 of Transducers). The derivative is the
12	output that $f$ still produces after having read $w$ ; for a function computed
13	by a Mealy machine it is determined by the state reached after reading $w$ , which
14	is the observation behind the Myhill–Nerode lemma for Mealy machines (Lemma
15	A.2.10): a function is computed by a Mealy machine if and only if it is
16	letter-to-letter, its $n$ -th output letter depends only on the first $n$ input
17	letters, and it has finitely many derivatives. The minimal Mealy machine of such
18	a function has the derivatives as its states.
19
20	# Formalization notes
21
22	`deriv f w v` drops the first `w.length` letters of `f (w ++ v)`. An earlier
23	edition of the book wrote `f(w\_)(v) = f(wv)` without removing the output
24	produced while reading `w`; with that reading even the identity function has
25	infinitely many derivatives and Lemma A.2.10 fails, so the definition above is
26	the one the book now prints and the one its proof uses. No length preservation
27	is required of `f` for the definition to make sense.
28	-/
29
30	namespace Lax765601.Derivatives
31
32	/-- The derivative `f(w_)` of `f`: the output `f` produces after having read `w`,
33	namely `v ↦ f (w v)` with the first `\|w\|` letters of the output removed. -/
34	def deriv {A B : Type} (f : List A → List B) (w : List A) : List A → List B :=
35	fun v => (f (w ++ v)).drop w.length
36
37	end Lax765601.Derivatives
38

Formalization notes

$deriv f w v$ drops the first $w.length$ letters of $f (w ++ v)$ . An earlier edition of the book wrote $f(w\_)(v) = f(wv)$ without removing the output produced while reading $w$ ; with that reading even the identity function has infinitely many derivatives and Lemma A.2.10 fails, so the definition above is the one the book now prints and the one its proof uses. No length preservation is required of $f$ for the definition to make sense.

Builds on

none

Used by

Lax765601.MealyDerivatives

From Mathlib

Mathlib.Data.List.Basic

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive