FOP/ex8.3 - 大久保弘崇

ex8.10

puls3 :: () -> Bit
puls3 () = c where
  a = delay high c
  b = delay low a
  c = delay low b
 

「3番目」というのが0から数えてだと面倒なことになる。

ex8.11

nビット幅のdelayを1つ使う解

puls k () = o where
  (o:os) = delay ini (os++[o])
  ini = replicate (k-1) low ++ [high]
 

問題8.10の構造を生成する解

puls' k () = o where
  chain 0 = id
  chain n = delay low ->- chain (n-1)
  o = (delay high ->- chain (k-1)) o
 

あえてrowを使う解

puls'' k () = o where
  (_,o) = row (\(c,a)->(undefined,delay a c)) (o, high:replicate (k-1) low)
 

ex8.12

2進数を用いて状態を表す。
回路的に表すと、このような流れを作ればよい。

ex812 n () = o where
  w = width 1 0
  width w k = if n <= k then w else width (w*2) (k+1)
  sn = encode n
  encode 0 = []
  encode k | k `mod` 2 == 0 = low : rest
           | otherwise      = high: rest
    where rest = encode (k `div` 2)
  s1 = delay (replicate w low) s0
  (s2,_) = bitAdder (high,s1)
  s3 = foldr (curry or2) low $ zipWith (curry xor2) s2 sn
  o = inv s3
  s0 = andn (s2,s3)
 
andn :: ([Bit], Bit) -> [Bit]
andn (as, b) = map (curry and2 b) as
 

ex8.13

http://www.cse.chalmers.se/edu/course/TDA956/Papers/lava-tutorial.pdf
(was http://ittc.ku.edu/Projects/SLDG/filing_cabinet/claessen00tutorial.pdf)
の6章に順序回路の検証に関する説明がある。これに従って考える。

ex813 = prop_puls_ex812_same4len
prop_puls_ex812_same4len k inp = ok where
  out1 = puls'' k inp
  out2 = ex812 k inp
  ok = out1 <==> out2
 

これで型は正しく作られるのだが、satzoo (minisat)による自動証明を試みると

Satzoo: *** Exception: evaluating a delay component

と怒られる。verify関数なら起動までいくが、起動スクリプトがないので実際どうなるか試せず。

ex8.14

その続きに、片方だけ検証する性質が例示されているので引用する。

prop_ToggleEdgeIdentity inp = ok where
  mid = toggle ink
  out = edge mid
  ok = out <==> inp
 

両向きを同時に検証したかったら、常にhighが出るような回路でも組むのだろうか。

ex8.15

脈絡なく簡単すぎる。

counterUp :: Int -> Bit -> [Bit]
counterUp n inp = number where
  number = delay (zeroList n) number'
  (number', cout) = bitAdder (inp,number)
 

コメント