Initial commit

*.ibc

*.o

{-

This file defines types for different types of automata and functions for analyzing them.

-}

module Data.Automata

import Data.Fin

%default total

%access export

||| Interface for things that accept (or reject) strings over an alphabet.

interface Acceptor a alph where

    decide : a -> List alph -> Bool

||| A type for deterministic finite automata (DFA)

|||

||| @ state The type of the states

||| @ alph The type of the input symbols

data DFA : (state : Type) -> (alph : Type) -> Type where 

    ||| Makes a DFA

    |||

    ||| @ delta The state transition function

    ||| @ start The starting state

    ||| @ accepting The states that accept

    MkDFA : (delta : state -> alph -> state) -> (start : state) -> (accepting : List state) -> DFA state alph

||| Runs a DFA with an input string starting at a given state

runDFAFrom : DFA state alph -> state -> List alph -> state

runDFAFrom _ state [] = state

runDFAFrom a@(MkDFA delta _ _) st (x::xs) = runDFAFrom a (delta st x) xs

||| Runs a DFA with an input string

runDFA : DFA state alph -> List alph -> state

runDFA a@(MkDFA _ start _) xs = runDFAFrom a start xs

Eq state => Acceptor (DFA state alph) alph where

    decide a@(MkDFA _ _ accepting) xs = (runDFA a xs) `elem` accepting

||| A type for non-deterministic finite automata (NFA)

|||

||| @ state The type of the states

||| @ alph The type of the input symbols

data NFA : (state : Type) -> (alph : Type) -> Type where

    ||| Makes a NFA

    |||

    ||| @ delta The state transition function

    ||| @ start The starting state

    ||| @ accepting The states that accept

    MkNFA : (delta : state -> alph -> List state) -> (start : state) -> (accepting : List state) -> NFA state alph

||| Runs a NFA with an input string starting at a given state

runNFAFrom : NFA state alph -> state -> List alph -> List state

runNFAFrom _ state [] = [state]

runNFAFrom a@(MkNFA delta _ _) st (x::xs) = delta st x >>= (\y => runNFAFrom a y xs)

||| Runs a NFA with an input string

runNFA : NFA state alph -> List alph -> List state

runNFA a@(MkNFA _ start _) xs = runNFAFrom a start xs

Eq state => Acceptor (NFA state alph) alph where

    decide a@(MkNFA _ _ accepting) xs = any (`elem` accepting) (runNFA a xs)

||| Transforms a DFA into a NFA

DFAToNFA : DFA state alph -> NFA state alph

DFAToNFA a@(MkDFA delta start accepting) = MkNFA (\st, x => [delta st x]) start accepting

||| A type for non-deterministic finite automata with ε-transitions (ε-NFA)

|||

||| @ state The type of the states

||| @ alph The type of the input symbols

data ENFA : (state : Type) -> (alph : Type) -> Type where

    ||| Makes an ε-NFA

    |||

    ||| @ delta The state transition function

    ||| @ start The starting state

    ||| @ accepting The states that accept

    MkENFA : (delta : state -> Maybe alph -> List state) -> (start : state) -> (accepting : List state) -> ENFA state alph

-- TODO: make total (breadth-/depth-first-search?)

partial runENFAEpsilon : ENFA state alph -> state -> List state

runENFAEpsilon a@(MkENFA delta _ _) st = (delta st Nothing) >>= (\x => runENFAEpsilon a x)

partial runENFAFrom : ENFA state alph -> state -> List alph -> List state

runENFAFrom _ state [] = [state]

runENFAFrom a@(MkENFA delta _ _) st (x::xs) = (delta st (Just x) ++ runENFAEpsilon a st) >>= (\y => runENFAFrom a y xs)

module Main

import Data.Automata

import Data.Fin