-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathpointed-word.cabal
90 lines (71 loc) · 3.81 KB
/
pointed-word.cabal
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
cabal-version: 3.0
name: pointed-word
version: 0.1.0.0
synopsis:
A package for modeling pointed words: sequences with ≥ 0 focused elements.
description:
This package models the domain of /(multi)pointed words/ and mild generalizations, motivated by their uses in the formal language and automata theory:
- Modeling particular classes of state machines ("bimachines", "lookaround machines") over sequences.
- Reasoning about compositions of cokleisli arrows in list-zipper-like comonads.
- Modeling diffs of same-length sequences — or patches between them.
= What's a __pointed word__?
A /pointed word/ over /a/ consists of a sequence of points, with a (possibly empty) context on either side of the points. For the sake of documentation, /\>/ and /\</ are metalinguistic symbols that surround (point at) a pointed symbol. Examples:
- /abba\>x\<aaa\>y\</ is a (multi)pointed word with /abba/ and /aaa/ as contexts, and /x/ and /y/ as points.
- /\>x\<ay/ is a (singly-)pointed word with /ay/ as its only context, and /x/ as its only pointed symbol.
- /\>x\<\>y\</ is a pointed word with no contexts, and /x/ and /y/ as points.
- /xy/ is an unpointed word with /xy/ as its only context.
Points can be /introduced/ or /projected off/:
- /point 1 axb = a\>x\<b/
- /unpoint 1 a\>x\<b = axb/
Pointed words can be /concatenated/:
- /a\>x\<b ⋅ \>y\<a = a\>x\<b\>y\<a/
The set of all pointed words whose unpointed word /w/ of length /n/ is the same — e.g. /xyz/ form a finite Boolean (powerset) lattice:
- The /bottom element/ is the unpointed word /w/ — /xyz/.
- The /top element/ is the multipointed form of /w/ with /n/ points — /\>x\<\>y\<\>z\</.
- The /meet/ of two pointed forms /l ∧ r/ of /w/ is the pointed word with the set of points common to both /l/ and /r/ — /\>x\<yz ∧ xy\>z\< = xyz/.
- The /join/ of two pointed forms /l ∨ r/ of /w/ is the pointed word with the set of points present in at least one of /l/ and /r/ — /\>x\<yz ∨ xy\>z\< = \>x\<y\>z\</.
Two pointed words of the same length can be conveniently compared for substitution differences:
> a x ba y a z ab
> Δ a t ba u a v ab
> ≡ ( a>x<ba>y<a>z<ab
> , a>t<ba>u<a>v<ab
> )
That's the basic idea.
As described in more detail in the main module of the package, we can also generalize the notion of pointed word and context here to replace a context of actual symbols with some other type that represents a summary of that context — a state or run of states produced by an automaton.
license: MIT
license-file: LICENSE
author: Eric Meinhardt
maintainer: [email protected]
copyright: 2023
homepage: https://github.com/emeinhardt/pointed-word
bug-reports: https://github.com/emeinhardt/pointed-word/issues
category: Data
build-type: Simple
extra-doc-files: CHANGELOG.md
source-repository head
type: git
location: https://github.com/emeinhardt/pointed-word/pointed-word.git
common warnings
ghc-options: -Wall -Wdefault -Wno-orphans -Wredundant-constraints -Wincomplete-uni-patterns -Wincomplete-record-updates -Wcompat
library
import: warnings
hs-source-dirs: src
default-language: GHC2021
default-extensions:
UnicodeSyntax
other-extensions:
OverloadedLists
DerivingStrategies
DeriveAnyClass
exposed-modules:
PointedWord
PointedWord.Eps
PointedWord.Core
build-depends:
base >= 4.16 && < 5.0
, deepseq >= 1.4 && < 2.0
, base-unicode-symbols >= 0.2 && < 1.0
, composition >= 1.0 && < 1.1
, newtype-generics >= 0.6 && < 0.7
, containers >= 0.6 && < 0.7
, nonempty-containers >= 0.3 && < 0.4