Révision 201

CSL17/soundness.tex (revision 201)
12 12 
The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions.
13 13 
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.
14 14 

  		





  
  15
  
    

  		





  15
  16
  
    
\begin{definition}


  		





  16
  17
  
    
[Length bounded basic functions]


  		





  17
  18
  
    
We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:


  		





  18
  19
  
    
\[


  		





  19
  20
  
    
x \mode l = y \mode l


  		





  20
  21
  
    
\]


  		





  
  22
  
    
which is definable by safe recursion on $l$:


  		





  
  23
  
    
\[


  		





  
  24
  
    
\begin{array}{rcl}


  		





  
  25
  
    
\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\


  		





  
  26
  
    
\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y ))  )


  		





  
  27
  
    
\end{array}


  		





  
  28
  
    
\]


  		





  21
  29
  
    
\end{definition}


  		





  22
  30
  
    

  		





  23
  31
  
    
\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}


  		












  

    
      CSL17/ph-macros.tex	(revision 201)
    
  






  43
  43
  
    
\newcommand{\pair}[3]{\langle ; #1,#2 , #3 \rangle}


  		





  44
  44
  
    
\newcommand{\eq}{\textsc{eq}}


  		





  45
  45
  
    
\newcommand{\leqfn}{\textsc{leq}}


  		





  46
  
  
    
\newcommand{\bit}{\textsc{Bit}}


  		





  
  46
  
    
\newcommand{\bit}{\textsc{bit}}


  		





  
  47
  
    
\newcommand{\andfn}{\textsc{and}}


  		





  
  48
  
    
\newcommand{\orfn}{\textsc{or}}


  		





  
  49
  
    
\newcommand{\notfn}{\textsc{not}}


  		





  
  50
  
    
\newcommand{\equivfn}{\textsc{equiv}}


  		





  47
  51
  
    

  		





  48
  52
  
    
\newcommand{\zerobit}{\textsc{0bit}}


  		





  49
  53
  
    
\newcommand{\onebit}{\textsc{1bit}}


  		












  

    
      CSL17/preliminaries.tex	(revision 201)
    
  






  137
  137
  
    

  		





  138
  138
  
    
%\nb{TODO: extend with $\mu$s.}


  		





  139
  139
  
    

  		





  
  140
  
    
\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }


  		





  140
  141
  
    

  		





  
  142
  
    
\begin{example}


  		





  
  143
  
    
	[Some simple functions]


  		





  
  144
  
    
	\label{ex:simple-bc-fns}


  		





  
  145
  
    
	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}


  		





  
  146
  
    
	\todo{$\bit$}


  		





  
  147
  
    
	


  		





  
  148
  
    
	$\bit(l;x)$ returns the $\mode l$th bit of $x$.


  		





  
  149
  
    
	\end{example}


  		





  
  150
  
    

  		





  
  151
  
    

  		





  141
  152
  
    
\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}


  		





  142
  153
  
    

  		





  143
  154
  
    
Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, defined by using predicative minimization: 


  		












Formats disponibles :
  Unified diff