以下の内容はhttps://yoshisaur.hatenablog.jp/entry/2023/02/12/074728より取得しました。

オートマトン

最終的な成績

Aでした

課題に関するファイル

これ

1.1 論文管理ソフト

この問題を解く

Agda に関する論文を探して Zoteroに登録する
登録したものの Bibtex を export して、それをレポートせよ
論文に対する短いコメントをつけること

Zoteroをダウンロードする

Agda に関する論文を探して Zoteroに登録する

登録したものの Bibtex を export して、それをレポートする

  • ファイルが追加されていることを確認したら、Add to Collection → New Collection... → automatonと入力して保存
  • ファイルを副クリックして、Export Item
  • Eport Itemの設定
  • assignment_1_1.bibとして保存
  • 中身を$ cat assignment_1.bib | pbcopyでもメモ帳で開いてでもいいので、クリップボードに張ってメールのレポートに貼る、bibファイルも添付する
@article{_gearsoshoare_2019,
    title = {{GearsOSのHoare} {Logicをベースにした検証手法}},
    volume = {IEICE-118},
    url = {https://ken.ieice.org/ken/paper/20190116d1Jm/},
    abstract = {Gears OS は継続を主とするプログラミング言語 CbC で記述されている。OS やアプリケーションの信頼性を上げるには仕様を満たしていることを確認する必要がある。現在 GearsOS の仕様の確認には定理証明系である Agda を用いている。CbC では関数呼び出しを用いず goto 文により遷移する。これは Agda 上では継続渡しの記述を用いた関数として記述する。また、継続にはある関数を実行するための事前条件や事後条件などをもたせることが可能である。Hoare Logic では事前条件が成り立っているときにある関数を実行して、それが停止する際に事後条件を満たすことを確認する。これは継続を用いた Agda 上では事前条件を継続で関数に渡し、関数からさらに継続した先で事後条件が成り立つという形で記述できる。本発表では GearsOS の仕様確認に Hoare Logic をベースとした記述と証明を導入する。},
    language = {ja},
    number = {IEICE-MSS-384,IEICE-SS-385},
    urldate = {2023-02-11},
    journal = {IEICE Conferences Archives},
    author = {政尊, 外間 and 真治, 河野},
    month = jan,
    year = {2019},
    note = {Publisher: The Institute of Electronics, Information and Communication Engineers},
    pages = {IEICE--MSS},
}

論文に対する短いコメントをつける

while文を使ったプログラムが正しく機能することをagdaで証明しているところが興味深かった。
これがきっかけで卒論ではデータベースをcbcで実装し、その機能の信頼性をagdaで証明したものを書きたいと思った。

2.2 Agdaによる関数と証明

この問題を解く

以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。

解答

record1.agda

module record1 where

record _∧_ (A B : Set) : Set where
  field
     π1 : A
     π2 : B

ex0 : {A B : Set} → A ∧ B →  A
ex0 =  _∧_.π1 

ex1 : {A B : Set} → ( A ∧ B ) → A 
ex1 a∧b =  _∧_.π1 a∧b

open _∧_

ex0' : {A B : Set} → A ∧ B →  A
ex0' =  π1 

ex1' : {A B : Set} → ( A ∧ B ) → A 
ex1' a∧b =  π1 a∧b

ex2 : {A B : Set} → ( A ∧ B ) → B 
ex2 a∧b = π2 a∧b

--               [ A ]₁  [ B ]₂
--   ─────────────────────────────────────────── λ-elim
--                    A ∧ B
--   ─────────────────────────────────────────── λ-intro₂
--                    B → (A ∧ B)
--   ─────────────────────────────────────────── λ-intro₁
--                A → B → (A ∧ B)
ex3 : {A B : Set} → A → B → ( A ∧ B ) 
ex3 a b = record { π1 = a ; π2 = b }

--               [ A ]₁  [ A ]₂
--   ─────────────────────────────────────────── λ-elim
--                   (A ∧ A)
--   ─────────────────────────────────────────── λ-intro₁
--                    A → (A ∧ A)
ex4 : {A B : Set} → A → ( A ∧ A ) 
ex4 a  = record { π1 = a ;  π2 = a }

--                                   [B]₁  [C]₂
--                                 ───────────────────────────── λ-elim
--                     [ A ]₁          (B∧C) 
--   ─────────────────────────────────────────────────────────── λ-elim
--                          A    B       C
--   ─────────────────────────────────────────────────────────── λ-elim
--                         ( A ∧ B)      C
--   ─────────────────────────────────────────────────────────── λ-elim
--                              A ∧ (B∧C)
--   ─────────────────────────────────────────────────────────── λ-intro₁
--                    ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 

ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
ex5 a∧b∧c = record { π1 = π1 (π1 a∧b∧c) ; π2 = record { π1 = π2 (π1 a∧b∧c) ; π2 = π2 a∧b∧c } }

--
--                                 [(A → B ) ∧ ( B →  C) ]₁  
--                                ──────────────────────────────────── π1
--     [(A → B ) ∧ ( B →  C) ]₁        (A → B )    [A]₂
--   ──────────────────────────── π2 ─────────────────────── λ-elim
--          ( B →  C)                     B
--   ─────────────────────────────────────────── λ-elim
--                   C
--   ─────────────────────────────────────────── λ-intro₂
--                 A → C
--   ─────────────────────────────────────────── λ-intro₁
--     ( (A → B ) ∧ ( B →  C) )  → A → C
ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
ex6 x a = π2 x (π1 x a)

--         [ A ]₁  [ B ]₂
--   ──────────────────── λ-elim
--               B                  C
--   ─────────────────────────────────────────── λ-elim
--                       C
--   ─────────────────────────────────────────── λ-intro₃
--                     A → C
--   ─────────────────────────────────────────── λ-intro₂
--               ( B →  C) → A → C
--   ─────────────────────────────────────────── λ-intro₁
--          (A → B ) → ( B →  C)   → A → C
ex6' : {A B C : Set} →  (A → B ) → ( B →  C)   → A → C
ex6' = λ z z₁ z₂ → z₁ (z z₂)

実行

$ agda record1.agda && echo done
done

5.1 正規表現

この問題を解く

egrep / Perl などを使って、これらのパターンに対するテストプログラムを作成せよ。C で書くとどうなるか?

C の regcomp を使ってみよ。

perlで実装する

regex_match.perl

use strict;
use warnings;

my $target = "Brouhaha!";
my $regex = '(h|a)aha*';

while ($target =~ m/$regex/g) {
  my $match = $&;
  my $start = $-[0];
  my $end = $+[0];
  print "pattern match succeeded\n";
  print "Match: $match\n";
}

実行結果

$ perl regex_match.perl
pattern match succeeded
Match: haha

Cで実装する

regex_match.perl

#include <stdio.h>
#include <regex.h>
#include <stdlib.h>
#include <string.h>

int main(int argc, char *argv[]) {
  regex_t preg;
  int result, i, match_count;
  regmatch_t *pmatch;
  char *target = "Brouhaha!";
  int target_len = strlen(target);
  int offset = 0;

  // Compile the regular expression pattern
  result = regcomp(&preg, "(h|a)aha*", REG_EXTENDED);
  if (result != 0) {
    printf("fail to compile regex\n");
    return 1;
  }

  // Perform the pattern matching
  pmatch = malloc(sizeof(regmatch_t));
  result = regexec(&preg, target + offset, 1, pmatch, 0);
  match_count = 0;
  while (result == 0 && offset < target_len) {
    printf("pattern match succeeded\n");
    printf("Match: %.*s\n", (int)(pmatch[0].rm_eo - pmatch[0].rm_so), target + offset + pmatch[0].rm_so);
    match_count++;
    offset += pmatch[0].rm_eo;
    pmatch = realloc(pmatch, (match_count + 1) * sizeof(regmatch_t));
    result = regexec(&preg, target + offset, 1, &pmatch[match_count], REG_NOTBOL);
  }
  if (result != REG_NOMATCH) {
    printf("fail to execute regrex\n");
    return 1;
  }
  free(pmatch);

  regfree(&preg);

  return 0;
}

実行結果:

$ gcc regex_match.c -o regex_match && ./regex_match
pattern match succeeded
Match: haha

6.1 正規表現の決定性オートマトンへの変換

この問題を解く

以下の正規表現をDFAに変換せよ。

(1) (a*|b*)c

(2) (a|b)*c

(3) (a*|b*)c(a|b)*c

(4) ((a*|b*)c)|((a|b)*c)

draw.ioなどで以下の図を再現して、svgで出力して学科ページに貼ればいいじゃないかと思う、それか画像を直接メールに添付でもいいかもしれないがどうだろう...?

一応、学科ページにdraw.ioで再利用可能なxmlファイルとsvgファイルをアップロードした、ご自由に再利用してください

index.html

<!doctype html>
<html lang="ja">
  <head>
    <meta charset="UTF-8">
    <title>automaton 6.1</title>
  </head>
  <body>
    <h1>automaton 6.1</h1>
    <hr>
    <h2>(1) (a*|b*)c</h2>
    <img src="images/6.1.1.svg">
    <a href="download/6.1.1.xml" download>xmlファイルのダウンロード</a>
    <hr>
    <h2>(2) (a|b)*c</h2>
    <img src="images/6.1.2.svg">
    <a href="download/6.1.2.xml" download>xmlファイルのダウンロード</a>
    <hr>
    <h2>(3) (a*|b*)c(a|b)*c</h2>
    <img src="images/6.1.3.svg">
    <a href="download/6.1.3.xml" download>xmlファイルのダウンロード</a>
    <hr>
    <h2>(4) ((a*|b*)c)|((a|b)*c)</h2>
    <img src="images/6.1.4.svg">
    <a href="download/6.1.4.xml" download>xmlファイルのダウンロード</a>
  </body>
</html>

ファイル構成

+amane+e205723 ls
download/  images/  index.html
+amane+e205723 ls download
6.1.1.xml  6.1.2.xml  6.1.3.xml  6.1.4.xml
+amane+e205723 ls images
6.1.1.svg  6.1.2.svg  6.1.3.svg  6.1.4.svg
+amane+e205723 pwd
/home/student/e20/e205723/public_html/automaton/6-1
  • (1) (a*|b*)c
  • (2) (a|b)*c
  • (3) (a*|b*)c(a|b)*c
  • (4) ((a*|b*)c)|((a|b)*c)


以上の内容はhttps://yoshisaur.hatenablog.jp/entry/2023/02/12/074728より取得しました。
このページはhttp://font.textar.tv/のウェブフォントを使用してます
不具合報告/要望等はこちらへお願いします。
モバイルやる夫Viewer Ver0.14