Skip to content

Instantly share code, notes, and snippets.

@brokenpylons

brokenpylons/dual.ml

Last active January 4, 2023 12:07
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save brokenpylons/c0a5a2971ff3a1a02278e3d7515b5d55 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save brokenpylons/c0a5a2971ff3a1a02278e3d7515b5d55 to your computer and use it in GitHub Desktop.
Download ZIP
Direct implemention of the extended dual regular expressions due to Alexander Okhotin
Raw
dual.ml
(* Extended dual regular expressions (Alexander Okhotin: The dual of concatenation).
The dual of constants is their complement.
The dual of the union is the intersection defined as DualUnion (x, y) = (Comp (Union (Comp x) (Comp y))).
The dual of the concatenation is defined analogously as DualConcat (x, y) = (Comp (Concat (Comp x) (Comp y))).
Other dual operations are constructed out of these duals in the customary way.
The duals are essentially just the "upside-down" versions of the operations.
The derivatives of the dual operations are constructed out of the duals in the customary way.
The compliment is implemented by replacing the operations with their duals.
It is computed in advance.
It is unclear whether the duals or the compliment represent the better base set of operations.
Plus:
The operations do not modify the meaning of other operations.
Minus:
Since the duals and their operations are just "upside-down" copies, everything is repeated twice.
*)
module Abstract = struct
type 'a t =
| Nothing
| DualNothing
| Null
| DualNull
| Lits of 'a
| DualLits of 'a
| Concat of bool * 'a t * 'a t
| DualConcat of bool * 'a t * 'a t
| Union of bool * 'a t * 'a t
| DualUnion of bool * 'a t * 'a t
| Repeat of bool * 'a t * int
| DualRepeat of bool * 'a t * int
| Star of 'a t
| DualStar of 'a t
[@@deriving eq, ord]
type 'a lits = 'a
let pp pp_lits =
let rec go ppf = function
| Nothing -> Fmt.string ppf "∅"
| DualNothing -> Fmt.string ppf "Σ*"
| Null -> Fmt.string ppf "ε"
| DualNull -> Fmt.string ppf "Σ⁺"
| Lits x -> pp_lits ppf x
| DualLits x -> Fmt.pf ppf "@[[@[%a@]]@]" pp_lits x
| Concat (_, x, y) -> Fmt.pf ppf "@[@[%a@]@ @[%a@]@]" go x go y
| DualConcat (_, x, y) -> Fmt.pf ppf "@[@[%a@]@,#@,@[%a@]@]" go x go y
| Union (_, x, y) -> Fmt.pf ppf "@[(@[%a@]@,|@,@[%a@])@]" go x go y
| DualUnion (_, x, y) -> Fmt.pf ppf "@[(@[%a@]@,&@,@[%a@])@]" go x go y
| Repeat (_, x, i) -> Fmt.pf ppf "@[%a@,@[{%i}@]@]" go x i
| DualRepeat (_, x, i) -> Fmt.pf ppf "@[%a@,@[-{%i}@]@]" go x i
| Star x -> Fmt.pf ppf "@[(@[%a@]){*}@]" go x
| DualStar x -> Fmt.pf ppf "@[(@[%a@])-{*}@]" go x
in go
let is_nullable = function
| Nothing -> false
| DualNothing -> true
| Null -> true
| DualNull -> false
| Lits _ -> false
| DualLits _ -> true
| Concat (m, _, _) -> m
| DualConcat (m, _, _) -> m
| Union (m, _, _) -> m
| DualUnion (m, _, _) -> m
| Repeat (m, _, _) -> m
| DualRepeat (m, _, _) -> m
| Star _ -> true
| DualStar _ -> false
let nothing =
Nothing
let dual_nothing =
DualNothing
let null =
Null
let dual_null =
DualNull
let lits s =
Lits s
let dual_lits s =
DualLits s
let concat x y =
Concat (is_nullable x && is_nullable y, x, y)
let dual_concat x y =
DualConcat (is_nullable x || is_nullable y, x, y)
let union x y =
Union (is_nullable x || is_nullable y, x, y)
let dual_union x y =
DualUnion (is_nullable x && is_nullable y, x, y)
let repeat x = function
| 0 -> Repeat (true, x, 0)
| i when i > 0 -> Repeat (is_nullable x, x, i)
| _ -> assert false
let dual_repeat x = function
| 0 -> DualRepeat (false, x, 0)
| i when i > 0 -> DualRepeat (is_nullable x, x, i)
| _ -> assert false
let star x =
Star x
let dual_star x =
DualStar x
let rec comp = function
| Nothing -> DualNothing
| DualNothing -> Nothing
| Null -> DualNull
| DualNull -> Null
| Lits s -> DualLits s
| DualLits s -> Lits s
| Concat (m, x, y) -> DualConcat (not m, comp x, comp y)
| DualConcat (m, x, y) -> Concat (not m, comp x, comp y)
| Union (m, x, y) -> DualUnion (not m, comp x, comp y)
| DualUnion (m, x, y) -> Union (not m, comp x, comp y)
| Repeat (m, x, i) -> DualRepeat (not m, comp x, i)
| DualRepeat (m, x, i) -> Repeat (not m, comp x, i)
| Star x -> DualStar (comp x)
| DualStar x -> Star (comp x)
end
module type LITS = sig
type t
val pp: t Fmt.t
val equal: t -> t -> bool
val compare: t -> t -> int
val subset: t -> t -> bool
end
module Concrete(Lits: LITS) = struct
include Abstract
type t = Lits.t Abstract.t
[@@deriving eq, ord, show]
let first =
let rec go = function
| Nothing -> Seq.empty
| DualNothing -> Seq.empty
| Null -> Seq.empty
| DualNull -> Seq.empty
| Lits p -> Seq.return p
| DualLits p -> Seq.return p
| Concat (_, x, y) when is_nullable x -> Seq.append (go x) (go y)
| Concat (_, x, _) -> go x
| DualConcat (_, x, _) when is_nullable x -> go x
| DualConcat (_, x, y) -> Seq.append (go x) (go y)
| Union (_, x, y) -> Seq.append (go x) (go y)
| DualUnion (_, x, y) -> Seq.append (go x) (go y)
| Repeat (_, x, _) -> go x
| DualRepeat (_, x, _) -> go x
| Star x -> go x
| DualStar x -> go x
in go
let rec simplify = function
| Union (m, x, y) ->
(match simplify x, simplify y with
| Union (n, x, y), z -> Union (m, x, Union (n, y, z))
| Nothing, x -> x
| x, Nothing -> x
| DualNothing, _ -> DualNothing
| _, DualNothing -> DualNothing
| x, y when equal x y -> x
| x, y when compare x y > 0 -> Union (m, y, x)
| x, y -> Union (m, x, y))
| DualUnion (m, x, y) ->
(match simplify x, simplify y with
| DualUnion (n, x, y), z -> DualUnion (m, x, DualUnion (n, y, z))
| Nothing, _ -> Nothing
| _, Nothing -> Nothing
| DualNothing, x -> x
| x, DualNothing -> x
| x, y when equal x y -> x
| x, y when compare x y > 0 -> DualUnion (m, y, x)
| x, y -> DualUnion (m, x, y))
| Concat (m, x, y) ->
(match simplify x, simplify y with
| Concat (n, x, y), z -> Concat (m, x, Concat (n, y, z))
| Nothing, _ -> Nothing
| _, Nothing -> Nothing
| Null, x -> x
| x, Null -> x
| DualNothing, DualNothing -> DualNothing
| DualNull, DualNull -> DualNull
| x, y -> Concat (m, x, y))
| DualConcat (m, x, y) ->
(match simplify x, simplify y with
| DualConcat (n, x, y), z -> DualConcat (m, x, DualConcat (n, y, z))
| DualNothing, _ -> DualNothing
| _, DualNothing -> DualNothing
| DualNull, x -> x
| x, DualNull -> x
| Nothing, Nothing -> Nothing
| Null, Null -> Null
| x, y -> DualConcat (m, x, y))
| Repeat (_, _, 0) -> Null
| Repeat (m, x, i) ->
(match simplify x with
| Nothing -> Nothing
| Null -> Null
| DualNothing -> DualNothing
| DualNull -> DualNull
| x -> Repeat (m, x, i))
| DualRepeat (_, _, 0) -> DualNull
| DualRepeat (m, x, i) ->
(match simplify x with
| Nothing -> Nothing
| Null -> Null
| DualNothing -> DualNothing
| DualNull -> DualNull
| x -> DualRepeat (m, x, i))
| Star x ->
(match simplify x with
| Null -> Null
| Nothing -> Null
| DualNothing -> DualNothing
| DualNull -> DualNothing
| Star x -> x
| x -> Star x)
| DualStar x ->
(match simplify x with
| Null -> Nothing
| Nothing -> Nothing
| DualNothing -> DualNull
| DualNull -> DualNull
| DualStar x -> x
| x -> DualStar x)
| x -> x
let rec derivative s = function
| Nothing -> nothing
| DualNothing -> dual_nothing
| Null -> nothing
| DualNull -> dual_nothing
| Lits p ->
if Lits.subset s p
then null
else nothing
| DualLits p ->
if Lits.subset s p
then dual_null
else dual_nothing
| Concat (_, x, y) when is_nullable x -> union (concat (derivative s x) y) (derivative s y)
| Concat (_, x, y) -> concat (derivative s x) y
| DualConcat (_, x, y) when is_nullable x -> dual_concat (derivative s x) y
| DualConcat (_, x, y) -> dual_union (dual_concat (derivative s x) y) (derivative s y)
| Union (_, x, y) -> union (derivative s x) (derivative s y)
| DualUnion (_, x, y) -> dual_union (derivative s x) (derivative s y)
| Repeat (_, x, i) ->
(match i with
| 0 -> nothing
| i -> concat (derivative s x) (repeat x (pred i)))
| DualRepeat (_, x, i) ->
(match i with
| 0 -> dual_nothing
| i -> dual_concat (derivative s x) (dual_repeat x (pred i)))
| Star x ->
concat (derivative s x) (star x)
| DualStar x ->
dual_concat (derivative s x) (dual_star x)
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment