Skip to content

Commit

Permalink
π’Ÿ ; Clarify tries as "automatic differentiation".
Browse files Browse the repository at this point in the history
  • Loading branch information
@conal
conal committed Feb 27, 2021
1 parent 3e38fad commit 74705d6
Show file tree
Hide file tree
Showing 7 changed files with 132 additions and 67 deletions.
2 changes: 2 additions & 0 deletions Automatic.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,9 @@ open Lang
\end{code}
\end{minipage}
\hfill\;
\ifacm\else
\vspace{-3.5ex}
\fi
\begin{center}
\begin{code}
βˆ… : Lang β—‡.βˆ…
Expand Down
138 changes: 86 additions & 52 deletions Calculus.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ module Calculus {β„“} (A : Set β„“) where
open import Data.Sum
open import Data.Product
open import Data.List
open import Data.List.Properties using (++-identityΚ³)
open import Function using (id; _∘_; _↔_; mk↔′)
open import Relation.Binary.PropositionalEquality hiding ([_])

Expand All @@ -26,20 +27,42 @@ private
B : Set b
X : Set b
P Q : Lang

f : A ✢ β†’ B
u v w : A ✢
\end{code}

%<*Ξ½Ξ΄>
%<*Ξ½π’Ÿ>
\AgdaTarget{Ξ½, Ξ΄}
\begin{code}
Ξ½ : (A ✢ β†’ B) β†’ B -- β€œnullable”
Ξ½ : (A ✢ β†’ B) β†’ B -- β€œnullable”
Ξ½ f = f []

Ξ΄ : (A ✢ β†’ B) β†’ A β†’ (A ✢ β†’ B) -- β€œderivative”
δ f a = f ∘ (a ∷_)
π’Ÿ : (A ✢ β†’ B) β†’ A ✢ β†’ (A ✢ β†’ B) -- β€œderivative”
π’Ÿ f u v = f (u βŠ™ v)
\end{code}
%% π’Ÿ f u = f ∘ (u βŠ™_)
%</Ξ½π’Ÿ>

%<*Ξ΄>
\begin{code}
Ξ΄ : (A ✢ β†’ B) β†’ A β†’ (A ✢ β†’ B)
Ξ΄ f a = π’Ÿ f [ a ]
\end{code}
%</Ξ΄>

%<*π’Ÿ[]βŠ™>
\begin{code}
π’Ÿ[] : π’Ÿ f [] ≑ f

π’ŸβŠ™ : π’Ÿ f (u βŠ™ v) ≑ π’Ÿ (π’Ÿ f u) v
\end{code}
\begin{code}[hide]
π’Ÿ[] = refl

π’ŸβŠ™ {u = []} = refl
π’ŸβŠ™ {f = f} {u = a ∷ u} = π’ŸβŠ™ {f = Ξ΄ f a} {u = u}
\end{code}
%% δ f a as = f (a ∷ as)
%</Ξ½Ξ΄>
%</π’Ÿ[]βŠ™>

%<*foldl>
\begin{code}[hide]
Expand All @@ -53,11 +76,36 @@ private
\end{code}
%</foldl>

%<*Ξ½βˆ˜π’Ÿ>
\begin{code}
Ξ½βˆ˜π’Ÿ : βˆ€ (f : A ✢ β†’ B) β†’ Ξ½ ∘ π’Ÿ f β‰— f
\end{code}
\begin{code}[hide]
Ξ½βˆ˜π’Ÿ f u rewrite (++-identityΚ³ u) = refl

-- Ξ½βˆ˜π’Ÿ f u = cong f (++-identityΚ³ u)

-- Ξ½βˆ˜π’Ÿ f [] = refl
-- Ξ½βˆ˜π’Ÿ f (a ∷ as) = Ξ½βˆ˜π’Ÿ (Ξ΄ f a) as
\end{code}
%</Ξ½βˆ˜π’Ÿ>

%<*π’Ÿfoldl>
\begin{code}
π’Ÿfoldl : π’Ÿ f β‰— foldl Ξ΄ f
\end{code}
\begin{code}[hide]
π’Ÿfoldl [] = refl
π’Ÿfoldl (a ∷ as) = π’Ÿfoldl as
\end{code}
%</π’Ÿfoldl>

%% Phasing out. Still used in talk.tex.
%<*ν∘foldlδ>
\AgdaTarget{ν∘foldlδ}
%% ν∘foldlΞ΄ : βˆ€ w β†’ P w ≑ Ξ½ (foldl Ξ΄ P w)
\begin{code}
ν∘foldlΞ΄ : Ξ½ ∘ foldl Ξ΄ P β‰— P
ν∘foldlΞ΄ : Ξ½ ∘ foldl Ξ΄ f β‰— f
ν∘foldlδ [] = refl
ν∘foldlδ (a ∷ as) = ν∘foldlδ as
\end{code}
Expand Down Expand Up @@ -175,41 +223,41 @@ private
(Ξ» { (([] , .(a ∷ w)) , refl , Ξ½P , Qaw) β†’ refl
; ((.a ∷ u , v) , refl , Pu , Qv) β†’ refl })

Ξ½β˜† {P = P} = mk↔′ f f⁻¹ invΛ‘ invΚ³
Ξ½β˜† {P = P} = mk↔′ k k⁻¹ invΛ‘ invΚ³
where
f : Ξ½ (P β˜†) β†’ (Ξ½ P) ✢
f zeroβ˜† = []
f (sucβ˜† (([] , []) , refl , (Ξ½P , Ξ½Pβ˜†))) = Ξ½P ∷ f Ξ½Pβ˜†
k : Ξ½ (P β˜†) β†’ (Ξ½ P) ✢
k zeroβ˜† = []
k (sucβ˜† (([] , []) , refl , (Ξ½P , Ξ½Pβ˜†))) = Ξ½P ∷ k Ξ½Pβ˜†

f⁻¹ : (Ξ½ P) ✢ β†’ Ξ½ (P β˜†)
f⁻¹ [] = zeroβ˜†
f⁻¹ (Ξ½P ∷ Ξ½P✢) = sucβ˜† (([] , []) , refl , (Ξ½P , f⁻¹ Ξ½P✢))
k⁻¹ : (Ξ½ P) ✢ β†’ Ξ½ (P β˜†)
k⁻¹ [] = zeroβ˜†
k⁻¹ (Ξ½P ∷ Ξ½P✢) = sucβ˜† (([] , []) , refl , (Ξ½P , k⁻¹ Ξ½P✢))

invΛ‘ : βˆ€ (Ξ½P✢ : (Ξ½ P) ✢) β†’ f (f⁻¹ Ξ½P✢) ≑ Ξ½P✢
invΛ‘ : βˆ€ (Ξ½P✢ : (Ξ½ P) ✢) β†’ k (k⁻¹ Ξ½P✢) ≑ Ξ½P✢
invΛ‘ [] = refl
invˑ (νP ∷ νP✢) rewrite invˑ νP✢ = refl

invΚ³ : βˆ€ (Ξ½Pβ˜† : Ξ½ (P β˜†)) β†’ f⁻¹ (f Ξ½Pβ˜†) ≑ Ξ½Pβ˜†
invΚ³ : βˆ€ (Ξ½Pβ˜† : Ξ½ (P β˜†)) β†’ k⁻¹ (k Ξ½Pβ˜†) ≑ Ξ½Pβ˜†
invΚ³ zeroβ˜† = refl
invΚ³ (sucβ˜† (([] , []) , refl , (Ξ½P , Ξ½Pβ˜†))) rewrite invΚ³ Ξ½Pβ˜† = refl

Ξ΄β˜† {P}{a} {w} = mk↔′ f f⁻¹ invΛ‘ invΚ³
Ξ΄β˜† {P}{a} {w} = mk↔′ k k⁻¹ invΛ‘ invΚ³
where
f : Ξ΄ (P β˜†) a w β†’ ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w
f (sucβ˜† (([] , .(a ∷ w)) , refl , (Ξ½P , Pβ˜†a∷w))) with f Pβ˜†a∷w
k : Ξ΄ (P β˜†) a w β†’ ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w
k (sucβ˜† (([] , .(a ∷ w)) , refl , (Ξ½P , Pβ˜†a∷w))) with k Pβ˜†a∷w
... | νP✢ , etc
= νP ∷ νP✢ , etc
f (sucβ˜† ((.a ∷ u , v) , refl , (Pa∷u , Pβ˜†v))) = [] , (u , v) , refl , (Pa∷u , Pβ˜†v)
k (sucβ˜† ((.a ∷ u , v) , refl , (Pa∷u , Pβ˜†v))) = [] , (u , v) , refl , (Pa∷u , Pβ˜†v)

f⁻¹ : ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w β†’ Ξ΄ (P β˜†) a w
f⁻¹ ([] , (u , v) , refl , (Pa∷u , Pβ˜†v)) = (sucβ˜† ((a ∷ u , v) , refl , (Pa∷u , Pβ˜†v)))
f⁻¹ (Ξ½P ∷ Ξ½P✢ , etc) = (sucβ˜† (([] , a ∷ w) , refl , (Ξ½P , f⁻¹ (Ξ½P✢ , etc))))
k⁻¹ : ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w β†’ Ξ΄ (P β˜†) a w
k⁻¹ ([] , (u , v) , refl , (Pa∷u , Pβ˜†v)) = (sucβ˜† ((a ∷ u , v) , refl , (Pa∷u , Pβ˜†v)))
k⁻¹ (Ξ½P ∷ Ξ½P✢ , etc) = (sucβ˜† (([] , a ∷ w) , refl , (Ξ½P , k⁻¹ (Ξ½P✢ , etc))))

invΛ‘ : (s : ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w) β†’ f (f⁻¹ s) ≑ s
invΛ‘ : (s : ((Ξ½ P) ✢ Β· (Ξ΄ P a ⋆ P β˜†)) w) β†’ k (k⁻¹ s) ≑ s
invΛ‘ ([] , (u , v) , refl , (Pa∷u , Pβ˜†v)) = refl
invˑ (νP ∷ νP✢ , etc) rewrite invˑ (νP✢ , etc) = refl

invΚ³ : (s : Ξ΄ (P β˜†) a w) β†’ f⁻¹ (f s) ≑ s
invΚ³ : (s : Ξ΄ (P β˜†) a w) β†’ k⁻¹ (k s) ≑ s
invΚ³ (sucβ˜† (([] , .(a ∷ w)) , refl , (Ξ½P , Pβ˜†a∷w))) rewrite invΚ³ Pβ˜†a∷w = refl
invΚ³ (sucβ˜† ((.a ∷ u , v) , refl , (Pa∷u , Pβ˜†v))) = refl

Expand All @@ -218,44 +266,30 @@ private

Clarify the relationship with automatic differentiation:

\begin{code}
π’Ÿ : (A ✢ β†’ B) β†’ A ✢ β†’ (A ✢ β†’ B)
π’Ÿ f u v = f (u ++ v)
\end{code}

\begin{code}
private
variable
f : A ✢ β†’ B
u v w : A ✢
\end{code}
\begin{code}
π’Ÿfoldl : π’Ÿ f β‰— foldl Ξ΄ f
π’Ÿfoldl [] = refl
π’Ÿfoldl (a ∷ as) = π’Ÿfoldl as

π’Ÿ[_] : Ξ΄ f a ≑ π’Ÿ f [ a ]
π’Ÿ[_] = refl
\end{code}

Now enhance \AF π’Ÿ:
%<*π’Ÿβ€²>
\begin{code}
π’Ÿβ€² : (A ✢ β†’ B) β†’ A ✢ β†’ B Γ— (A ✢ β†’ B)
π’Ÿβ€² f u = f u , π’Ÿ f u
\end{code}
%</π’Ÿβ€²>

%<*Κ»π’Ÿ>
\begin{code}
Κ»π’Ÿ : (A ✢ β†’ B) β†’ A ✢ β†’ B Γ— (A ✢ β†’ B)
Κ»π’Ÿ f u = Ξ½ fβ€² , fβ€² where fβ€² = foldl Ξ΄ f u
-- Κ»π’Ÿ f u = let fβ€² = foldl Ξ΄ f u in Ξ½ fβ€² , fβ€²
\end{code}
%% Κ»π’Ÿ f u = let fβ€² = foldl Ξ΄ f u in Ξ½ fβ€² , fβ€²
%</Κ»π’Ÿ>

%<*π’Ÿβ€²β‰‘Κ»π’Ÿ>
\begin{code}
-- π’Ÿβ€²foldl : βˆ€ u β†’ π’Ÿβ€² f u ≑ let fβ€² = foldl Ξ΄ f u in Ξ½ fβ€² , fβ€²
π’Ÿβ€²foldl : π’Ÿβ€² f β‰— Κ»π’Ÿ f
π’Ÿβ€²foldl [] = refl
π’Ÿβ€²foldl (a ∷ as) = π’Ÿβ€²foldl as
π’Ÿβ€²β‰‘Κ»π’Ÿ : π’Ÿβ€² f β‰— Κ»π’Ÿ f
\end{code}
\begin{code}[hide]
π’Ÿβ€²β‰‘Κ»π’Ÿ [] = refl
π’Ÿβ€²β‰‘Κ»π’Ÿ (a ∷ as) = π’Ÿβ€²β‰‘Κ»π’Ÿ as
\end{code}
%</π’Ÿβ€²β‰‘Κ»π’Ÿ>

\note{There's probably a way to \AK{rewrite} with \AB{π’Ÿfoldl} and \AB{π’Ÿβ€²foldl} to eliminate the induction here.}

2 changes: 2 additions & 0 deletions SizedAutomatic.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,9 @@ open Lang
\end{code}
\end{minipage}
\hfill\;
\ifacm\else
\vspace{-3.5ex}
\fi
\begin{center}
\begin{code}
βˆ… : Lang i β—‡.βˆ…
Expand Down
2 changes: 2 additions & 0 deletions Symbolic.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,9 @@ data Lang : β—‡.Lang β†’ Set (suc β„“) where
_β—‚_ : (Q ⟷ P) β†’ Lang P β†’ Lang Q
\end{code}
\end{center}
\ifacm\else
\vspace{-5ex}
\fi
\hfill
\begin{minipage}[t]{33ex}
\begin{code}
Expand Down
3 changes: 2 additions & 1 deletion To do.md
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
## To do

* Restore some of the removed "powerful perspectives" text in the calculus section.
* Conclusions and future work.
* Clarify tries as "automatic differentiation".
* Read over `Predicate.Properties` and see what might be worth mentioning.
For instance, distributivity of concatenation over union generalizes to mapping.

Expand Down Expand Up @@ -59,6 +59,7 @@ From old paper version to-do:

## Did

* Clarify tries as "automatic differentiation".
* Mention the *non-idempotence* of this notion of languages, due to choice of equivalence relation.
* Maybe mention logical equivalence vs proof isomorphism again in the Related Work section.
* Wouter's paper
Expand Down
44 changes: 31 additions & 13 deletions paper.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,20 +162,27 @@
\sectionl{Decomposing Languages}
\rnc\source{Calculus}

In order to convert languages into parsers, it will help to decompose languages into a regular form.
Since lists are defined by an algebraic data type, we can decompose languages---and indeed any function from lists---according to constructor, as follows:
\agda{Ξ½Ξ΄}
In terms of languages, {\AF{δ} \AB{P} \AB{a}} comprises all strings \AB{w} such that {\AB{a} \AIC ∷ \AB{w}} is in \AB{P}\out{, i.e., the tails of strings in \AB{P} that start with \AB{a}}.

Each use of \AF{Ξ΄} takes us one step closer to reducing general language membership to nullability.
In other words,\footnote{For functions \AB{f} and \AB{g}, {\AB{f} \AF{β‰—} \AB{g}} is extensional equality, i.e., {\AS βˆ€ \AB x \AS β†’ \AB{f} \AB{x} \AD{≑} \AB{g} \AB{x}}.
Repeated application is expressed as a standard left fold\out{ \stdlibCitep{Data.List}}:
In order to convert languages into parsers, it will help to understand how language membership relates to the algebraic structure of lists, specifically the monoid formed by \AIC{[]} and \AF{\_βŠ™\_}.
Generalizing from languages to functions from lists to \emph{any} type, define
\agda{Ξ½π’Ÿ}
In terms of languages, {\AF{π’Ÿ} \AB{P} \AB{u}} comprises all strings \AB{v} such that {\AB{u} \AF βŠ™ \AB{v} \AF ∈ \AB{P}}, i.e., \AB{u}-suffixes of strings in \AB{P}.

Since {\AB{u} \AF βŠ™ \AIC{[]} \AD ≑ \AB{u}}, it follows that\footnote{For functions \AB{f} and \AB{g}, {\AB{f} \AF{β‰—} \AB{g}} is extensional equality, i.e., {\AS βˆ€ \AB x \AS β†’ \AB{f} \AB{x} \AD{≑} \AB{g} \AB{x}}.}
\agda{Ξ½βˆ˜π’Ÿ}
Moreover, the function \AF{π’Ÿ} distributes over \AIC{[]} and \AF{\_βŠ™\_}:\out{\footnote{In algebraic terms, argument-flipped \AF{π’Ÿ} is a monoid homomorphism from lists to language endofunctions.}}
\agda{π’Ÿ[]βŠ™}
These facts suggest that \AB{π’Ÿ} can be computed one list element at a time via a more specialized operation, as is indeed the case:\footnote{Repeated \AF{Ξ΄} application is expressed as a standard left fold\out{ \stdlibCitep{Data.List}}:
\agda{foldl}\vspace{-2ex}
}%
\agda{ν∘foldlδ}
}
\agda{Ξ΄}
\agda{π’Ÿfoldl}
Each use of \AF{Ξ΄} thus takes us one step closer to reducing general language membership to nullability.
%% In other words,%
%% \agda{ν∘foldlδ}
This simple observation is the semantic heart of the syntactic technique of \emph{derivatives of regular expressions} as used for efficient recognition of regular languages \citep{Brzozowski64}, later extended to parsing general context-free languages \citep{Might2010YaccID}.
Lemma \AF{ν∘foldlδ} liberates this technique from the assumption that languages are represented \emph{symbolically}, by some form of grammar (e.g., regular or context-free), inviting other representations as we will see in \secref{Automatic Differentiation}.
Lemmas \AF{Ξ½βˆ˜π’Ÿ} and \AF{π’Ÿfoldl} liberate this technique from the assumption that languages are represented \emph{symbolically}, by some form of grammar (e.g., regular or context-free), inviting other representations as we will see in \secref{Automatic Differentiation}.

\begin{comment}
Lemma \AF{ν∘foldlδ} relates to some other powerful perspectives and principles as well:
\begin{itemize}

Expand All @@ -192,6 +199,7 @@
\emph{Calculus}: \AB{δ} is differentiation; {\AF{ν} \AF ∘ \AF{foldl} \AF{δ} \AB{P}} is integration; and lemma \AF{ν∘foldlδ} is the second fundamental theorem of calculus, which says that a function can be recovered by integrating its derivative\out{ \needcite{}}.

\end{itemize}
\end{comment}

Given the definitions of \AF{Ξ½} and \AF{Ξ΄} above and of the language operations in \secref{Specifying Languages}, one can prove properties about how they relate, as shown in
\figrefdef{nu-delta-lemmas}{Properties of \AF{Ξ½} and \AF{Ξ΄} for language operations}{\agda{Ξ½Ξ΄-lemmas}}.
Expand Down Expand Up @@ -304,7 +312,17 @@
Decidable recognition is defined exactly as with unsized tries (\figref{automatic-defs}), with the sole exception of removing the compiler pragma that suppressed termination checking.
This time the compiler successfully proves \emph{total} correctness (including termination).

%% To more clearly see the parallel with automatic differentiation, note that
\rnc\source{Calculus}

To more clearly see the parallel with automatic differentiation (AD), note that AD implementations generally sample a function \emph{and} its derivative together to exploit the fact that these two computations typically share much common work.
This work sharing also applies when differentiating languages.
Without this optimization we have
\agda{π’Ÿβ€²}
The more efficient, work-sharing version:
\agda{Κ»π’Ÿ}
Their equivalence follows from lemmas \AF{Ξ½βˆ˜π’Ÿ} and \AF{π’Ÿfoldl} of \secref{Decomposing Languages}:
\agda{π’Ÿβ€²β‰‘Κ»π’Ÿ}
The trie representation accomplishes this sharing by weaving \AF{Ξ½} and \AF{Ξ΄} into a single structure based on common prefixes.


\sectionl{Generalizing from languages to predicates}
Expand Down Expand Up @@ -341,7 +359,7 @@
\agda{domain-transformers}
\end{minipage}
\hfill\;
} shows two parallel collections of predicate operations, each covariantly transforming the codomain (left) or domain (right).\footnote{The types of operations on the left can be further relaxed from \AF{Set β„“} to any codomain type, while keeping \AB{A} fixed, resulting in the usual covariant applicative functor of functions \emph{from} a fixed type \citep{McBride2008APE}.
} shows two parallel collections of predicate operations, each covariantly transforming the codomain (left) or domain (right).\footnote{The types of operations on the left can be further relaxed from {\APT{Set} \AB β„“} to any codomain type, while keeping \AB{A} fixed, resulting in the usual covariant applicative functor of functions \emph{from} a fixed type \citep{McBride2008APE}.
Dually, the operations on the right (in their current generality) form a covariant applicative functor of functions \emph{to} types.}
These generalized operations then specialize to language operations as in \figrefdef{lang-via-pred}{Languages via predicate operations}{
\mathindent0ex
Expand Down
8 changes: 7 additions & 1 deletion unicode.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,7 @@
%% \newunicodechar{π“₯}{\ensuremath{\mathcal{V}}}
%% \newunicodechar{𝓦}{\ensuremath{\mathcal{W}}}

\newunicodechar{π’Ÿ}{\ensuremath{\mathscr{D}}}

%% Above I copied from gallais's TyDe'19 paper.
%% Below are my additions.
Expand All @@ -162,7 +163,12 @@

\newunicodechar{𝟏}{\ensuremath{\mathbf{1}}}

\newcommand\smallOp[2]{\ensuremath{\mathbin{\mbox{\raisebox{#1}{\scriptsize $#2$}}}}}
\ifacm
\newcommand\smallOpSize{\small}
\else
\newcommand\smallOpSize{\scriptsize}
\fi
\newcommand\smallOp[2]{\ensuremath{\mathbin{\mbox{\raisebox{#1}{\smallOpSize $#2$}}}}}
\newcommand\append{\smallOp{0.5pt}{+\!\!+}}

\newunicodechar{βŠ™}{\ensuremath{\append}}
Expand Down

0 comments on commit 74705d6

Please sign in to comment.