Skip to content

Commit fd7979a

Browse files
dnblndnbln
committed
updated quartz
1 parent fbc4554 commit fd7979a

File tree

253 files changed

+30323
-27
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

253 files changed

+30323
-27
lines changed

‎.github/workflows/publish.yaml‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
name: Deploy Quartz site to GitHub Pages
2+
3+
on:
4+
push:
5+
branches:
6+
- v4
7+
8+
permissions:
9+
contents: read
10+
pages: write
11+
id-token: write
12+
13+
concurrency:
14+
group: "pages"
15+
cancel-in-progress: false
16+
17+
jobs:
18+
build:
19+
runs-on: ubuntu-22.04
20+
steps:
21+
- uses: actions/checkout@v4
22+
with:
23+
fetch-depth: 0 # Fetch all history for git info
24+
- uses: actions/setup-node@v4
25+
with:
26+
node-version: 22
27+
- name: Install Dependencies
28+
run: npm ci
29+
- name: Build Quartz
30+
run: npx quartz build
31+
- name: Upload artifact
32+
uses: actions/upload-pages-artifact@v3
33+
with:
34+
path: public
35+
36+
deploy:
37+
needs: build
38+
environment:
39+
name: github-pages
40+
url: ${{ steps.deployment.outputs.page_url }}
41+
runs-on: ubuntu-latest
42+
steps:
43+
- name: Deploy to GitHub Pages
44+
id: deployment
45+
uses: actions/deploy-pages@v4

‎content/.gitkeep‎

Whitespace-only changes.

‎content/agdomaton-src/Agdomaton/DfaDef.lagda.md‎

Lines changed: 187 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,187 @@
1+
---
2+
title: DFA definition
3+
date: 2024-04-20
4+
published: 2024-04-20
5+
updated: 2024-04-20
6+
tags:
7+
- agdomaton
8+
growth-stage: seedling
9+
---
10+
11+
Contains the DFA definition.
12+
13+
## Imports
14+
15+
```agda
16+
module Agdomaton.DfaDef where
17+
18+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
19+
open import Data.Nat using (ℕ; zero; suc; _≤_; s≤s)
20+
open import Data.Empty using (⊥; ⊥-elim)
21+
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
22+
open import Data.Product using (_×_; _,_; proj₁; proj₂)
23+
open import Relation.Nullary using (¬_)
24+
open import Axiom.Extensionality.Propositional using (Extensionality)
25+
open import Data.List.Relation.Binary.Subset.Propositional.Properties
26+
open import Relation.Unary using (Pred; _⊆_; _∈_)
27+
open import Data.Fin.Base using (Fin; zero; suc; fromℕ; fromℕ<)
28+
open import Data.Vec using (Vec; _∷_; []; map)
29+
open import Agda.Builtin.List using (List; _∷_; [])
30+
open import Data.Bool.Base using (Bool; _∧_; true; false; if_then_else_)
31+
open import Agda.Primitive using (Set; Level; lzero; lsuc)
32+
33+
open import Agdomaton.LogicBase
34+
```
35+
36+
## Defining the DFA
37+
38+
```agda
39+
data State {n : ℕ} : Set where
40+
q : (Fin n) → State
41+
42+
data Symbol {n : ℕ} : Set where
43+
σ : (Fin n) → Symbol
44+
45+
-- A word, a list of symbols
46+
data Word {ns : ℕ} : ℕ → Set where
47+
[] : Word {ns} zero
48+
_∷_ : ∀ {n} (s : Symbol {ns}) (w : Word {ns} n) → Word {ns} (suc n)
49+
50+
-- A possibly infinite word, a list of symbols
51+
data IWord {ns : ℕ} : Set where
52+
[] : IWord {ns}
53+
_∷_ : (Symbol {ns}) → IWord {ns} → IWord {ns}
54+
55+
TransitionFunction : {nq ns : ℕ} → Set
56+
TransitionFunction {nq} {ns} = (State {nq} × Symbol {ns}) → State {nq}
57+
58+
record DFA
59+
{nq ns nf : ℕ}
60+
-- (Q : Vec (State {nq}) nq)
61+
-- (Σ : Vec (Symbol {ns}) ns)
62+
: Set where
63+
field
64+
δ : TransitionFunction {nq} {ns}
65+
q₀ : State {nq}
66+
F : Vec (State {nq}) nf
67+
```
68+
69+
## Helpers
70+
71+
```agda
72+
-- Check if two finite numbers are equal
73+
fin-eq : {n : ℕ}
74+
→ (Fin n)
75+
→ (Fin n)
76+
→ Bool
77+
fin-eq zero zero = true
78+
fin-eq zero (suc y) = false
79+
fin-eq (suc x) zero = false
80+
fin-eq (suc x) (suc y) = fin-eq x y
81+
82+
-- Check if two states are equal
83+
state-eq : {n : ℕ}
84+
→ State {n}
85+
→ State {n}
86+
→ Bool
87+
state-eq (q x) (q y) = fin-eq x y
88+
89+
-- Check if a state is in a vec of states
90+
elem-state : {nq n : ℕ}
91+
→ (State {nq})
92+
→ Vec (State {nq}) n
93+
→ Bool
94+
elem-state x [] = false
95+
elem-state x (y ∷ ys) = if (state-eq x y) then true else elem-state x ys
96+
97+
postulate
98+
all-symbols-impl : {ns : ℕ} → (n : ℕ) → (n ≤ (suc ns)) → Vec (Symbol {suc ns}) n
99+
-- all-symbols-impl {ns} zero n≤ns = []
100+
-- all-symbols-impl {ns} (suc n) n1≤ns = σ (fromℕ< {n} n1≤ns) ∷ all-symbols-impl {ns} n (s≤s n1≤ns)
101+
102+
postulate
103+
all-symbols : {ns : ℕ} → Vec (Symbol {ns}) ns
104+
-- all-symbols {zero} = []
105+
-- all-symbols {suc ns} = all-symbols-impl {ns} (suc ns)
106+
107+
all-true : {n : ℕ} → Vec Bool n → Bool
108+
all-true [] = true
109+
all-true (x ∷ xs) = x ∧ all-true xs
110+
111+
∀symbols-check : {ns : ℕ}
112+
→ ((Symbol {ns}) → Bool)
113+
→ Bool
114+
∀symbols-check {ns} p = all-true (map p (all-symbols {ns}))
115+
116+
∀symbols : {ns : ℕ}
117+
→ ((Symbol {ns}) → Bool)
118+
→ Bool
119+
∀symbols {ns} p = ∀symbols-check {ns} p
120+
121+
-- Follow a single symbol through a DFA, returning a new DFA which starts on
122+
-- the state reached by following the symbol
123+
dfa-transition-one : {nq ns nf : ℕ}
124+
→ (Symbol {ns})
125+
→ DFA {nq} {ns} {nf}
126+
→ DFA {nq} {ns} {nf}
127+
dfa-transition-one sym dfa = record dfa { q₀ = (DFA.δ dfa) ((DFA.q₀ dfa), sym) }
128+
129+
-- Check if a DFA is in an accept state.
130+
-- This checks if q₀ is in the set of accept states.
131+
dfa-in-accept-state : {nq ns nf : ℕ}
132+
→ DFA {nq} {ns} {nf}
133+
→ Bool
134+
dfa-in-accept-state dfa = elem-state (DFA.q₀ dfa) (DFA.F dfa)
135+
136+
cyclic-edge : {nq ns : ℕ}
137+
→ State {nq}
138+
→ Symbol {ns}
139+
→ TransitionFunction {nq} {ns}
140+
→ Bool
141+
cyclic-edge state sym δ = state-eq (δ (state , sym)) state
142+
143+
dead-state : {nq ns : ℕ}
144+
→ State {nq}
145+
→ TransitionFunction {nq} {ns}
146+
→ Bool
147+
dead-state state δ = ∀symbols (λ sym → cyclic-edge state sym δ)
148+
```
149+
150+
## Check if a DFA accepts a word
151+
152+
```agda
153+
-- Follow a word through a DFA, returning a
154+
-- new DFA which starts on the state reached
155+
-- by following the symbols.
156+
dfa-follow : {nq ns nf n : ℕ}
157+
→ Word {ns} n
158+
→ DFA {nq} {ns} {nf}
159+
→ DFA {nq} {ns} {nf}
160+
dfa-follow [] dfa = dfa
161+
dfa-follow (sym ∷ ss) dfa = dfa-follow ss (dfa-transition-one sym dfa)
162+
163+
-- Check if a DFA accepts a word.
164+
dfa-accepts : {nq ns nf n : ℕ}
165+
→ Word {ns} n
166+
→ DFA {nq} {ns} {nf}
167+
→ Bool
168+
dfa-accepts ls dfa = dfa-in-accept-state (dfa-follow ls dfa)
169+
170+
-- Follow a possibly infinite word through a DFA,
171+
-- returning a new DFA which starts on
172+
-- the state reached by following the symbols.
173+
dfa-follow-infinite : {nq ns nf : ℕ}
174+
→ IWord {ns}
175+
→ DFA {nq} {ns} {nf}
176+
→ DFA {nq} {ns} {nf}
177+
dfa-follow-infinite [] dfa = dfa
178+
dfa-follow-infinite (sym ∷ ss) dfa = dfa-follow-infinite ss (dfa-transition-one sym dfa)
179+
180+
-- Check if a DFA accepts a possibly infinite word.
181+
dfa-accepts-infinite : {nq ns nf n : ℕ}
182+
→ IWord {ns}
183+
→ DFA {nq} {ns} {nf}
184+
→ Bool
185+
dfa-accepts-infinite ls dfa = dfa-in-accept-state (dfa-follow-infinite ls dfa)
186+
```
187+

‎content/agdomaton-src/Agdomaton/LogicBase.lagda.md‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
---
2+
title: Base logic
3+
date: 2024-04-20
4+
published: 2024-04-20
5+
updated: 2024-04-20
6+
tags:
7+
- agdomaton
8+
growth-stage: seedling
9+
---
10+
11+
# Imports
12+
13+
```agda
14+
module Agdomaton.LogicBase where
15+
16+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
17+
open import Data.Nat using (ℕ; zero; suc)
18+
open import Data.Empty using (⊥; ⊥-elim)
19+
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
20+
open import Data.Product using (_×_; _,_; proj₁; proj₂)
21+
open import Relation.Nullary using (¬_)
22+
open import Axiom.Extensionality.Propositional using (Extensionality)
23+
open import Data.List.Relation.Binary.Subset.Propositional.Properties
24+
open import Relation.Unary using (Pred; _⊆_)
25+
```
26+
27+
# Definitions
28+
29+
```agda
30+
_⇔_ : Set → Set → Set
31+
A ⇔ B = (A → B) × (B → A)
32+
```
33+
34+
## Negation
35+
36+
```agda
37+
postulate
38+
¬¬-elim : {A : Set} → ¬ (¬ A) → A
39+
40+
¬¬¬-elim : {A : Set} → ¬ (¬ (¬ A)) → ¬ A
41+
¬¬¬-elim ¬¬¬A = λ a → ¬¬¬A (λ ¬A → ¬A a)
42+
```
43+
44+
# De Morgan laws
45+
46+
## De Morgan for disjunction
47+
48+
```agda
49+
de-morgan-or-forward : ∀ {A B : Set} → (¬ (A ⊎ B)) → ((¬ A) × (¬ B))
50+
de-morgan-or-forward ¬A⊎B = (λ a → ¬A⊎B (inj₁ a)) , (λ b → ¬A⊎B (inj₂ b))
51+
52+
de-morgan-or-backward : ∀ {A B : Set} → ((¬ A) × (¬ B)) → (¬ (A ⊎ B))
53+
de-morgan-or-backward ¬A׬B = [(proj₁ ¬A׬B), (proj₂ ¬A׬B)]
54+
55+
de-morgan-or : {A B : Set} → (¬ (A ⊎ B)) ⇔ ((¬ A) × (¬ B))
56+
de-morgan-or = de-morgan-or-forward , de-morgan-or-backward
57+
```
58+
59+
## De Morgan for conjunction
60+
61+
```agda
62+
postulate
63+
de-morgan-and-forward : ∀ {A B : Set} → (¬ (A × B)) → ((¬ A) ⊎ (¬ B))
64+
65+
de-morgan-and-backward : ∀ {A B : Set} → ((¬ A) ⊎ (¬ B)) → (¬ (A × B))
66+
de-morgan-and-backward ¬A⊎¬B A×B = [ (λ ¬A -> ¬A (proj₁ A×B)) , (λ ¬B → ¬B (proj₂ A×B) ) ] ¬A⊎¬B
67+
68+
de-morgan-and : {A B : Set} → (¬ (A × B)) ⇔ ((¬ A) ⊎ (¬ B))
69+
de-morgan-and = de-morgan-and-forward , de-morgan-and-backward
70+
```

‎content/agdomaton-src/Agdomaton/Main.lagda.md‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
---
2+
title: Main module
3+
date: 2024-04-21
4+
published: 2024-04-21
5+
updated: 2024-04-21
6+
tags:
7+
- agdomaton
8+
growth-stage: seedling
9+
---
10+
11+
## Import everything
12+
13+
```agda
14+
module Agdomaton.Main where
15+
16+
open import Agdomaton.LogicBase
17+
open import Agdomaton.DfaDef
18+
19+
20+
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
21+
open import Data.Nat using (ℕ; zero; suc)
22+
open import Data.Empty using (⊥; ⊥-elim)
23+
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_])
24+
open import Data.Product using (_×_; _,_; proj₁; proj₂)
25+
open import Relation.Nullary using (¬_)
26+
open import Axiom.Extensionality.Propositional using (Extensionality)
27+
open import Data.List.Relation.Binary.Subset.Propositional.Properties
28+
open import Relation.Unary using (Pred; _⊆_; _∈_)
29+
open import Data.Fin.Base using (Fin; zero; suc)
30+
open import Data.Vec using (Vec; _∷_; [])
31+
open import Agda.Builtin.List using (List; _∷_; [])
32+
open import Data.Bool.Base using (Bool; true; false; if_then_else_)
33+
open import Agda.Primitive using (Set)
34+
35+
open import Agda.Builtin.IO using (IO)
36+
open import Agda.Builtin.Unit using (⊤)
37+
open import Agda.Builtin.String using (String)
38+
```
39+
40+
## Test a basic DFA
41+
42+
```agda
43+
2-length-counter-transition : (State {2} × Symbol {2}) → State {2}
44+
2-length-counter-transition (q zero , _) = q (suc zero)
45+
2-length-counter-transition (q (suc zero) , _) = q zero
46+
47+
48+
2-length-counter : DFA {2} {2} {1}
49+
-- (q zero ∷ q (suc zero) ∷ [])
50+
-- (σ zero ∷ σ (suc zero) ∷ [])
51+
2-length-counter = record
52+
{ q₀ = q zero
53+
; δ = 2-length-counter-transition
54+
; F = q zero ∷ []
55+
}
56+
57+
58+
test-dfa : Bool
59+
test-dfa = dfa-accepts ((σ zero) ∷ (σ (suc zero)) ∷ []) 2-length-counter
60+
```
61+
62+
## Define main
63+
64+
```agda
65+
postulate putStrLn : String → IO ⊤
66+
{-# FOREIGN GHC import qualified Data.Text as T #-}
67+
{-# COMPILE GHC putStrLn = putStrLn . T.unpack #-}
68+
69+
show : Bool → String
70+
show true = "true"
71+
show false = "false"
72+
73+
main : IO ⊤
74+
main = putStrLn (show test-dfa)
75+
```

‎content/agdomaton-src/Agdomaton/index.md‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
---
2+
title: "Agdomaton"
3+
date: 2024-04-20
4+
published: 2024-04-20
5+
updated: 2024-04-20
6+
tags:
7+
- agdomaton
8+
growth-stage: seedling
9+
---
10+
11+
Agda proofs for Automata, Complexity, and Computability theory.
12+
13+
>[!todo]
14+
>Also check out [Zakrok09](https://github.com/Zakrok09/)'s [`ts-automata` TypeScript package](https://github.com/Zakrok09/ts-automata).

0 commit comments

Comments
 (0)