copy a few starter files

.gitignore

@@ -0,0 +1,3 @@
+latex/
+*.agdai
+

Makefile

@@ -0,0 +1,103 @@
+PAPER=language-derivatives
+
+# all: latex/$(PAPER).pdf
+all: talk
+
+talk:
+	make -C Talk
+
+.PHONY: talk
+
+MODULES:=\
+  Introduction \
+  Generation \
+  Predicate \
+  Closed/Structures \
+  Predicate/Properties \
+  Predicate/Algebra \
+  Nullability \
+  Inverses \
+  Decidability \
+  Calculus \
+  Regex \
+  Trie \
+  ProvingProperties \
+
+#   NonTrie \
+
+#   BeyondPredicates \
+#   Predicate/Examples \
+#   Predicate/Examples/Bit \
+#   Relation \
+#   Relation/Properties
+
+#   AltDec \
+#   AltCalc \
+#   NewIntroduction \
+
+LAGDAS:=$(patsubst %,%.lagda,$(MODULES))
+
+AGDA_DEPENDENCIES:=$(patsubst %,latex/%.tex,$(MODULES))
+.SECONDARY: $(AGDA_DEPENDENCIES)
+
+PAPER_DEPENDENCIES:= \
+  latex/$(PAPER).tex \
+  latex/bib.bib \
+  latex/macros.tex \
+  latex/unicode.tex \
+  latex/commands.tex \
+  $(AGDA_DEPENDENCIES)
+
+AGDA=agda
+
+# AGDA-EXTRAS=--only-scope-checking
+
+# AGDA-EXTRAS+=--termination-depth=2
+
+
+# latex/%.tex: %.lagda
+# 	@mkdir -p $(dir $@)
+# 	${AGDA} -i . --latex $(AGDA-EXTRAS) $< --latex-dir=latex > $(basename $@).log
+
+# POSTPROCESS=postprocess-latex.pl
+
+latex/%.tex: %.lagda
+	@mkdir -p $(dir $@)
+	${AGDA} -i . --latex $(AGDA-EXTRAS) $< --latex-dir=latex > $(basename $@).log
+
+# references option. Doesn't seem to work.
+
+# latex/%.tex: %.lagda Makefile
+# 	mkdir -p $(dir $@)
+# 	${AGDA} -i . --latex $(AGDA-EXTRAS) $< --latex-dir=latex > $(basename $@).log
+# 	perl $(POSTPROCESS) < $(basename $@).tex > $(basename $@).processed
+# 	mv $(basename $@).processed $(basename $@).tex
+
+latex/%: %
+	@mkdir -p $(dir $@)
+	cp $< $@
+
+latex/$(PAPER).pdf: $(PAPER_DEPENDENCIES)
+	cd latex && latexmk -xelatex -bibtex ${PAPER}.tex
+
+latex/Test.pdf: latex/Test.tex $(PAPER_DEPENDENCIES)
+	cd latex && latexmk -xelatex -bibtex Test.tex
+
+SHOWPDF=skim
+
+see: $(PAPER).see
+
+%.see: latex/%.pdf
+	${SHOWPDF} $<
+
+clean:
+	rm -r latex
+
+tags: $(LAGDAS)
+	etags $^
+
+web: web-token
+
+web-token: latex/$(PAPER).pdf
+	scp $< conal@conal.net:/home/conal/domains/conal/htdocs/papers/$(PAPER)
+	touch web-token

Misc.lagda

@@ -0,0 +1,79 @@
+\sectionl{Miscellaneous Definitions}
+
+\begin{code}
+{-# OPTIONS --safe --without-K #-}
+
+open import Level
+
+module Misc {ℓ : Level} where
+\end{code}
+
+\subsection{̄{⊥ and ⊤}
+
+Make ⊥ and ⊤ level-monomorphic to simplify signatures elsewhere.
+Doing so loses some generality, but that generality is already lost in equational reasoning on types.
+
+\begin{code}
+open import Data.Empty.Polymorphic using () renaming (⊥ to ⊥′)
+open import Data.Empty.Polymorphic using (⊥-elim) public
+open import Data.Unit.Polymorphic  using () renaming (⊤ to ⊤′)
+
+⊥ : Set ℓ
+⊥ = ⊥′
+
+⊤ : Set ℓ
+⊤ = ⊤′
+
+import Data.Unit
+pattern tt = lift Data.Unit.tt
+
+infix 3 ¬_
+¬_ : Set ℓ → Set ℓ
+¬ X = X → ⊥
+
+open import Data.Unit  using () renaming (tt to tt⇂) public
+open import Data.Empty using () renaming (⊥-elim to ⊥-elim⇂) public
+\end{code}
+
+
+\subsection{Lists}
+
+For succinctness and consistency with algebraically related notions, use star for list types.
+So that I can tweak the typesetting, rename append.
+
+\begin{code}
+open import Data.List
+
+infixl 10 _✶
+_✶ : Set ℓ → Set ℓ
+_✶ = List            
+
+infixr 5 _⊙_
+_⊙_ : ∀ {A} → A ✶ → A ✶ → A ✶
+_⊙_ = _++_
+\end{code}
+
+
+\subsection{Functions}
+
+\begin{code}
+open import Data.Product
+
+uncurry₃ˡ : ∀ {a b c d} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
+            {D : Σ (Σ A B) (uncurry C) → Set d} →
+            ((x : A) → (y : B x) → (z : C x y) → D ((x , y) , z)) →
+            ((p : _) → D p)
+uncurry₃ˡ f ((x , y) , z) = f x y z
+
+\end{code}
+
+\begin{code}
+private variable A B : Set ℓ
+\end{code}
+
+Agda doesn't like ``∃ λ (a , b) → ...'', maybe because it can't sort out how \AB{b} could depends on \AB{a}.
+I'd like to find a better solution.
+\begin{code}
+∃⇃ : (A × B → Set ℓ) → Set ℓ
+∃⇃ = ∃
+\end{code}

commands.tex

@@ -0,0 +1,23 @@
+%%%%%%%%%% AGDA ALIASES
+
+\newcommand{\APT}{\AgdaPrimitiveType}
+\newcommand{\AK}{\AgdaKeyword}
+\newcommand{\AM}{\AgdaModule}
+\newcommand{\AS}{\AgdaSymbol}
+\newcommand{\AStr}{\AgdaString}
+\newcommand{\AN}{\AgdaNumber}
+\newcommand{\AD}{\AgdaDatatype}
+\newcommand{\AF}{\AgdaFunction}
+\newcommand{\ARe}{\AgdaRecord}
+\newcommand{\AFi}{\AgdaField}
+\newcommand{\AB}{\AgdaBound}
+\newcommand{\AIC}{\AgdaInductiveConstructor}
+\newcommand{\AC}{\AgdaComment}
+\newcommand{\AG}{\AgdaGeneralizable}
+
+\newcommand{\Set}{\mathbf{Set}}
+
+\newcommand{\AR}{\AgdaRef}
+
+%% Targets I've turned off
+\newcommand\NoAgdaTarget[1]{}

language-derivatives.tex

@@ -0,0 +1,88 @@
+\documentclass[hidelinks]{article}  % fleqn,12pt
+\usepackage[margin=1in]{geometry}  % 0.12in, 0.9in, 1in
+
+\usepackage{catchfilebetweentags}
+\usepackage[useregional]{datetime2}
+
+%% \usepackage{balance}  % even out final two-column page
+
+\RequirePackage{newunicodechar, amssymb, stmaryrd, unicode-math, setspace}
+
+\input{commands}
+\input{unicode}
+\input{macros}
+
+\usepackage[links]{agda}% references
+
+%% Switching to \textsf for AgdaFunction messes up vertical alignment.
+%% \newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
+
+\renewcommand{\AgdaFontStyle}[1]{\text{#1}}
+
+%% \renewcommand{\AgdaFunction}[1]
+%%     {\AgdaNoSpaceMath{\text{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+%% \renewcommand{\AgdaRecord}[1]
+%%     {\AgdaNoSpaceMath{\text{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
+
+\author{Conal Elliott}
+
+\begin{document}
+
+%% \nc\tit{Working Title}
+\nc\tit{Symbolic and Automatic Differentiation of Languages}
+
+\title{\tit}
+\date{Early draft of \DTMnow}
+
+\maketitle
+
+\begin{abstract}
+Formal languages are usually defined in terms of set theory.
+Choosing type theory instead gives us languages as type-level predicates over strings.
+Applying a language to a string yields a type whose elements are language membership proofs describing \emph{how} a string parses in the language.
+The usual building blocks of languages (including union, contatenation, and Kleene closure) have precise and compelling specifications uncomplicated by operational strategies and are easily generalized to a few general domain-transforming and codomain-transforming operations on predicates.
+
+A simple type isomorphism property captures the essential idea behind language ``differentiation'' and ``integration'' as used for recognizing languages and leads to a collection of lemmas about type-level languages (and indeed functions from lists to any type).
+These lemmas form the backbone of two dual implementations of language recognition---(inductive) regular expressions and (coinductive) tries---each containing almost exactly the same code but in dual arrangements.
+The language lemmas form most of the implementation in both cases, while the representation and primitive operations trade places.
+The regular expression version corresponds to symbolic differentiation, while the trie version corresponds to automatic differentiation.
+
+The relatively easy-to-prove properties of type-level languages transfer almost effortlessly to the decidable implementations.
+In particular, despite the inductive and coinductive nature of regular expressions and tries respectively, we need neither inductive nor coinductive/bisumulation arguments to prove algebraic properties.
+\end{abstract}
+
+\renewcommand\AgdaTarget[1]{}
+
+%% \input{NewIntroduction}
+\input{Introduction}
+%% \input{Generation}
+\input{Predicate}
+%% \input{AltDec}
+%% \input{AltCalc}
+\input{Predicate/Algebra}
+\input{Nullability}
+\input{Decidability}
+\input{Calculus}
+% \input{NonTrie}
+\input{Regex}
+\input{Trie}
+\input{ProvingProperties}
+
+%% \input{BeyondPredicates}
+%% \input{Predicate/Examples}
+%% \input{Relation}
+
+\workingHere
+\note{To do: relate regular expressions and tries to symbolic and automatic differentiation; reflections, related work, future work.}
+
+%% \definecolor{mylinkcolor}{rgb}{0,0.4,0}
+%% \hypersetup{
+%%   linkcolor  = mylinkcolor,
+%%   citecolor  = mylinkcolor,
+%%   urlcolor   = mylinkcolor,
+%%   colorlinks = true
+%% }
+
+\bibliography{bib}
+
+\end{document}