[ new ] Levenshtein distance#3015
Conversation
| record Dist (xs ys : List A) (cost : ℕ) : Set (c ⊔ ℓ) where | ||
| constructor _,_ | ||
| field | ||
| edit : Edit xs ys cost | ||
| mini : ∀ cost' → Edit xs ys cost' → cost ≤ cost' | ||
| open Dist public | ||
|
|
||
| dist : Dist xs ys k → ℕ | ||
| dist {k = k} _ = k |
There was a problem hiding this comment.
Weird (of me) to home in on this item, but surprised that dist isn't simply given as a manifest field definition...?
| record Dist (xs ys : List A) (cost : ℕ) : Set (c ⊔ ℓ) where | |
| constructor _,_ | |
| field | |
| edit : Edit xs ys cost | |
| mini : ∀ cost' → Edit xs ys cost' → cost ≤ cost' | |
| open Dist public | |
| dist : Dist xs ys k → ℕ | |
| dist {k = k} _ = k | |
| record Dist (xs ys : List A) (cost : ℕ) : Set (c ⊔ ℓ) where | |
| constructor _,_ | |
| field | |
| edit : Edit xs ys cost | |
| mini : ∀ cost' → Edit xs ys cost' → cost ≤ cost' | |
| dist = cost | |
| open Dist public |
at which point, some reconsideration of the names might be in order?
There was a problem hiding this comment.
would it be useful to also define source and target extractors?
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Nice addition. Some questions (mostly), a couple of suggestions and a few minor changes.
| module Data.List.Relation.Binary.Distance.Levenshtein.Calc.DecPropositional | ||
| {a} {A : Set a} (_≡?_ : DecidableEquality A) where | ||
|
|
||
| open import Data.List.Base |
There was a problem hiding this comment.
I don't immediately see any uses of Data.List.Base in the rest of this file?
| open import Relation.Binary.Bundles using (Setoid; DecSetoid) | ||
| import Relation.Binary.Construct.On as On | ||
|
|
||
| -- should this go in Data.Char? |
There was a problem hiding this comment.
Yes, having this and the next in Data.Char is probably better than "buried" here.
| data Split {A : Set a} : Pred (List> A) a where | ||
| _||_ : (sx : List< A) → -- things to the left of the position | ||
| (xs : List> A) → -- things to the right of the position | ||
| Split (sx <>> xs) -- if we put things to the left & to the right side by side, |
There was a problem hiding this comment.
Isn't this green slime? Should this be forded? [More of a discussion point; things sure would be less pretty if it were forded.]
| ------------------------------------------------------------------------ | ||
| -- But (provided that A is inhabited) it is not a distance | ||
|
|
||
| -- These definitions surely need to go somewhere else |
There was a problem hiding this comment.
Function.Metric.Definitions ?
| -- Levenshtein distance: the Edit relation and its properties | ||
| ------------------------------------------------------------------------ | ||
|
|
||
| {-# OPTIONS --cubical-compatible --safe #-} |
There was a problem hiding this comment.
all need to change to --without-K !
| record Dist (xs ys : List A) (cost : ℕ) : Set (c ⊔ ℓ) where | ||
| constructor _,_ | ||
| field | ||
| edit : Edit xs ys cost | ||
| mini : ∀ cost' → Edit xs ys cost' → cost ≤ cost' | ||
| open Dist public | ||
|
|
||
| dist : Dist xs ys k → ℕ | ||
| dist {k = k} _ = k |
There was a problem hiding this comment.
would it be useful to also define source and target extractors?
|
|
||
| -- The relation is indeed unique | ||
| unique : Unique {A = List A} Dist | ||
| unique _ _ _ _ (dk , mk) (dl , ml) = ≤-antisym (mk _ dl) (ml _ dk) |
There was a problem hiding this comment.
Sure makes you wonder if unique's first 4 arguments (and triangle's even more below) should be implicit!
There was a problem hiding this comment.
I kept switching back and forth because when giving the counter examples in the
Edit file it sure is convenient to be able to talk about the extremities of the segments
you are measuring.
| ≤-trans (mlr m dlr′) m≤ | ||
|
|
||
|
|
||
| -- This should surely go somewhere else |
There was a problem hiding this comment.
Data.Nat.Relation.Ternary? Data.Nat.Relations ?
| ... | true = f refl | ||
| ... | false = t refl | ||
|
|
||
| m⊓′n⊓′o≤m : ∀ m n o → m ⊓′ n ⊓′ o ≤ m |
There was a problem hiding this comment.
This definitely belongs in Data.Nat.Properties (same with the next 2)
|
|
||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Known distances |
There was a problem hiding this comment.
Do these perhaps belong in Data.List.Relation.Binary.Distance.Levenshtein.Dist.Setoid.Properties ? (Would that be a depth record?)
3 participants
Sorry, it is a little bit of a code dump.
This is a generalisation of the coursework I set this year for our 4th years.
I have added
Text.Distance.Levenshteinto show how the setup can beused to compute the Levenshtein distance between two strings both in a
case sensitive and case insensitive manner.
Some things should be moved around but I am not exactly sure what to
call them and where to put them.
E.g. the case insensitive relation on characters and its properties should
probably go in the
Charhierarchy (what name for the relation?).Min3should probably also go somewhere else but I don't know where.I have introduced
Data.List.Relation.Unary.Splitbut it could just as wellbe understood as a data structure
Data.List.Splittogether with its ownrelation hierarchy containing the quantifier relation in
Data.List.Relation.Split.Relation.Unary.All.