[69143c]: web / entries / Functional-Automata.shtml  Maximize  Restore  History

Download this file

96 lines (82 with data), 2.8 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="front.css">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <meta name="GENERATOR" content="Quanta Plus">

<table width="100%">
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">

<!-- begin entry data: -->
<h1><!-- Title: -->Functional Automata</h1>

<table width="80%" class="data">
    <tr><td class="datahead" width="20%">Title:</td>
    <td class="data" width="80%">
<!-- Title: -->Functional Automata
    <tr><td class="datahead">Author:</td>
<td class="data">
<!-- Author: --><a
href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>
	<tr><td class="datahead">Submisison date:</td>
<td class="data"><!-- Submission date: -->2004-03-30</td></tr>

	<tr><td class="datahead" valign="top">Abstract:</td>
  <td class="abstract"> 
<!-- Abstract: -->	
This theory defines deterministic and nondeterministic automata in a
functional representation: the transition function/relation and the finality
predicate are just functions. Hence the state space may be infinite.  It is
shown how to convert regular expressions into such automata. A scanner
(generator) is implemented with the help of functional automata: the scanner
chops the input up into longest recognized substrings. Finally we also show
how to convert a certain subclass of functional automata (essentially the
finite deterministic ones) into regular sets.


<!-- entry directory name: -->
<!--#set var="name" value="Functional-Automata" -->

<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <td class="links">
	<a href="<!--#echo var="doc" -->">Proof document</a>
	<!-- link to README.hmtl if no document exists -->	
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
    <tr><td class="links">Older releases:	None</td></tr>
<!-- entry data end -->

</td> </tr> </table>
<div align="right" class="date">$Date: 2004-03-30 10:09:13 $, $Revision: 1.1 

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:

No, thanks