mod Ex03b

incl Mtex

incl Mtexln

incl Maux

loc rem 
  \para \bf  3. CVIČENIE Z PREDMETU 1-AIN-470 ŠPECIFIKÁCIA A VERIFIKÁCIA 
  PROGRAMOV  \end 

loc rem 
  \para* \it  Meno:  \end 
  \para* \it  Verzia CL:  \end 5.81.21.2 
  \para* \it  Dátum:  \end pondelok 27.2.2023 
  \para* \it  WWW:  \end 
  http://www.ii.fmph.uniba.sk/cl/view.php/courses/1-AIN-470-svp/2223ls/?lang=sk 
  \para* \it  Kontakt:  \end Jan.Komara(at)fmph.uniba.sk 

loc rem 
  \para \bf  Úvodná poznámka.  \end Toto cvičenie je venované týmto 
  témam: 
  \items 
   \item \para celočíselná odmocnina (názorný príklad), 
   \item \para Cantorova párovacia funkcia a aritmetizácia karteziánskeho 
         súčinu, 
   \item \para Catalanova párovacia funkcia. 
  \end
  \para Zadanie sa skladá z týchto súborov: 
  \items 
   \item \para Súbory \it  mtex*.cl  \end obsahujú makrá pre CL-TeX. 
   \item \para Súbory \it  maux*.cl  \end obsahujú definície a vlastnosti 
         pomocných funkcií a predikátov. 
   \item \para Súbory \it  ex*.cl  \end obsahujú úlohy, ktoré máte riešiť 
         na tomto cvičení. 
   \item \para Súbor \it  msyntax.cl  \end obsahuje základnú syntax systému 
         CL. 
  \end
  \para Tieto súbory sa musia skompilovať v správnom poradí. Presný postup 
  je uvedený v súbore \it  readme.txt  \end. 

loc rem 
  \para \bf  Hodnotenie.  \end 
  \items 
   \item \para Počet bodov za úlohy v tomto súbore: 1 
   \item \para Počet bodov za prémiove úlohy v tomto súbore: 0 
  \end
  \para Odovzdať do 4.3.2023 (sobota). 

loc rem 
  ******************************************************************************
  ********************************* EXERCISES **********************************
  ******************************************************************************

rem 
  \para \bf  Literature.  \end 
  \items 
   \item \para \it  [1]  \end J. Komara. Specification and Verification of 
         Programs. Online. 
   \item \para \it  [2]  \end Ján Kľuka. Úvod do deklaratívneho 
         programovania. Online. 
   \item \para \it  [3]  \end Ján Komara. Recursive Functions. Online. 
  \end

rem 
  \para \bf  [CL] Remark.  \end Catalan pairing function - see the module \it  
  Maux*  \end. 

rem 
  \para \bf  Chapter. Programs Operating on Lists.  \end 

rem 
  \para \bf  Section. Lists.  \end 

rem 
  \para \bf  List length.  \end 

fun L 
  L(0) = 0
  L(x,xs) = L(xs)+1

rem 
  \para \bf  List indexing.  \end 

fun/2 Sub 'Tex_f2_ln_sub'
  Sub(xs,i) = Proj1 Iproj2(i,xs)

rem 
  \para \bf  Section. Operations on Lists.  \end 

rem 
  \para \bf  Counting the number of occurrences in lists.  \end 

fun/2 Count 'Tex_f2_ln_count'
  Count(a,0) = 0
  Count(a,x,xs) = Eqf(a,x)+Count(a,xs)

rem 
  \para \bf  Section. Sorting of Lists.  \end 

rem 
  \para \bf  Permutations.  \end 

pred/2 Perm 'Tex_p2_ln_perm'
  Perm(xs,ys) <-> \a a Count(a,xs) = Count(a,ys)

rem 
  \para \bf  Ordered lists.  \end 

pred Ord 
  Ord(xs) <-> \a i\a j(i < j & j < L(xs) -> Sub(xs,i) <= Sub(xs,j))

rem 
  \para \bf  Subsection. Insertion Sort.  \end 

rem 
  \para \bf  Insertion function.  \end \header* fun/2 Insert  \end Define the 
  function \ft Insert(a,xs) \end such that 
  \eq* 
    Perm(Insert(a,xs),a,xs)
  \end
  \eq* 
    Ord(xs) -> Ord Insert(a,xs)
  \end

fun/2 Insert 
  Insert(a,xs) = Foo

rem 
  \para \bf  Insertion sort.  \end Implement insertion sort; that is, define the 
  function \ft Isort(x) \end such that 
  \eq* 
    Perm(Isort(xs),xs)
  \end
  \eq* 
    Ord Isort(xs)
  \end
  \para with the help of the insertion function \ft Insert(a,xs) \end. 

fun Isort 
  Isort(xs) = Foo

rem 
  \para \bf  Subsection. Merge Sort.  \end 

rem 
  \para \bf  [CL] Remark.  \end Below we will use the discrimination on whether 
  or not \ft L(xs) <= 1 \end. As we have 
  \eq* 
    L(xs) <= 1 <-> Tex_f1_pp_proj2(xs) = 0
  \end
  \para we may suppose that the test \ft L(xs) <= 1 \end takes constant time. 

rem 
  \para \bf  Splitting the list into two halves.  \end Define the function 
  \ft Msplit(xs) \end such that 
  \eq* 
    \e ys\e zs Msplit(xs) = ys,zs
  \end
  \eq* 
    Msplit(xs) = ys,zs -> Perm(xs,ys++zs)
  \end
  \eq* 
    Msplit(xs) = ys,zs -> L(ys) = L(zs) \/ L(ys) = L(zs)+1
  \end

fun Msplit 
  Msplit(xs) = Foo <- L(xs) <= 1
  Msplit(xs) = Foo <- L(xs) > 1

rem 
  \para \bf  Merging two ordered lists into one.  \end 
  \header* fun/2 Merge  \end Define the function \ft Merge(xs,ys) \end such that 
  \eq* 
    Perm(Merge(xs,ys),xs++ys)
  \end
  \eq* 
    Ord(xs) & Ord(ys) -> Ord Merge(xs,ys)
  \end

fun/2 Merge 
  Merge(xs,ys) = Foo

rem 
  \para \bf  Merge sort. \it  (1 point)  \end  \end Implement merge sort; that 
  is, define the function \ft Msort(xs) \end such that 
  \eq* 
    Perm(Msort(xs),xs)
  \end
  \eq* 
    Ord Msort(xs)
  \end
  \para with the help of \ft Msplit(xs) \end and \ft Merge(xs,ys) \end. 
  \para \it  [CL] Remark.  \end Clearly \ft L(xs) <= 1 <-> Proj2(xs) = 0 \end 
  and thus we may suppose that the discrimination on whether \ft L(xs) <= 1 \end 
  or not can be carried out in constant time. 

fun Msort 
  Msort(xs) = Foo <- L(xs) <= 1
  Msort(xs) = Foo <- L(xs) > 1

