Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/cbc-type.tex @ 81:3f63f697ed3a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Update
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Wed, 08 Feb 2017 17:37:08 +0900
parents 897fda8e39c5
children 39a27b704f0c
comparison
equal deleted inserted replaced
80:73da47f32888 81:3f63f697ed3a
1 \chapter{Agda における Continuation based C の表現} 1 \chapter{Agda における Continuation based C の表現}
2 \label{chapter:cbc-type} 2 \label{chapter:cbc-type}
3 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。 3 ~\ref{chapter:agda}章では Curry-Howard 同型対応により、型付きラムダ計算を用いて命題が証明できることを示した。
4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。 4 加えて、証明支援系言語 Agda を用いてデータの定義とそれを扱う関数の性質の証明が行なえることを確認した。
5 5
6 CbC で自身を証明するために依存型を利用したいが、CbC には専用の型システムが存在しない。
7 依存型を定義するためにもまず現状の CbC を型付けする必要がある。
8
6 この章では CbC の型システムを部分型を利用して定義する。 9 この章では CbC の型システムを部分型を利用して定義する。
7 定義した型システムがきちんと検査されるかを確認するため、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、型付けされることを確認する。 10 定義した型システムを用いて、Agda 上に DataSegment と CodeSegment の定義、CodeSegment の接続と実行、メタ計算を定義し、それらが型付けされることを確認する。
8 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda 証明する。 11 また、Agda 上で定義した DataSegment とそれに付随する CodeSegment の持つ性質を Agda で証明する。
9 12
10 % {{{ 部分型付け 13 % {{{ 部分型付け
11 14
12 \section{部分型付け} 15 \section{部分型付け}
16 TODO: なおす
13 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。 17 単純型付きラムダ計算では、ラムダ計算の項が型付けされることを確認した。
14 ここで、 単純型の拡張として、レコードを導入する。 18 ここで、 単純型の拡張として、レコードを導入する。
15 19
16 レコードとは名前の付いた複数の値を保持するデータである。 20 レコードとは名前の付いた複数の値を保持するデータである。
17 C 言語における構造体などがレコードに相当する。 21 C 言語における構造体などがレコードに相当する。
509 513
510 \verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。 514 \verb/pushSingleLinkedStack/ は \verb/element/ を新しく確保し、値を入れた後に \verb/next/ へと繋げ、 \verb/top/ を更新して軽量継続する。
511 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。 515 \verb/popSingleLinkedStack/ は先頭が空でなければ先頭の値を \verb/top/ から取得し、\verb/element/を一つ進める。
512 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。 516 値が空であれば \verb/data/ を \verb/NULL/ にしたまま軽量継続を行なう。
513 517
514 % TODO null check を入れる
515 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c} 518 \lstinputlisting[label=src:cbc-push-pop, caption= CbC における SingleLinkedStack を操作する Meta CodeSegment] {src/singleLinkedStack.c}
516 519
517 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。 520 次に Agda における定義をリスト~\ref{src:agda-push-pop}に示す。
518 同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。 521 同様に \verb/pushSingleLinkedStack/ と \verb/popSingleLinkedStack/ を定義している。
519 \verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。 522 \verb/pushsinglelinkedstack/ では、スタックの値を更新したのちにノーマルレベルの CodeSegment である \verb/n/ を \verb/exec/ している。