# HG changeset patch # User Yasutaka Higa # Date 1419486753 -32400 # Node ID 9d0c57803ca0eb7190dbf89f33126cc2fc127473 # Parent e233b786623e504d09d9707194897e1e58f6fede Add figure for description delta (apply function example) diff -r e233b786623e -r 9d0c57803ca0 figure/apply_function.graffle --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/figure/apply_function.graffle Thu Dec 25 14:52:33 2014 +0900 @@ -0,0 +1,1337 @@ + + + + + ActiveLayerIndex + 0 + ApplicationVersion + + com.omnigroup.OmniGraffle + 139.18.0.187838 + + AutoAdjust + + BackgroundGraphic + + Bounds + {{0, 0}, {558.99997329711914, 783}} + Class + SolidGraphic + ID + 2 + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + + BaseZoom + 0 + CanvasOrigin + {0, 0} + ColumnAlign + 1 + ColumnSpacing + 36 + CreationDate + 2014-12-25 05:16:49 +0000 + Creator + atton + DisplayScale + 1 0/72 in = 1 0/72 in + GraphDocumentVersion + 8 + GraphicsList + + + Bounds + {{68.624973297119141, 212}, {103, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 5 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 f(g(x))} + + + + Bounds + {{68.624973297119141, 172}, {103, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 4 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 f'(g'(x))} + + + + Bounds + {{68.624973297119141, 132}, {103, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 18 + + ID + 3 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 f'(g''(x))} + + + + Class + LineGraphic + ID + 40 + Points + + {402.0172910628728, 96.870333541118512} + {439.87498664855957, 121.99999535646094} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 38 + + + + Bounds + {{18.000001907348633, 212.00001525878906}, {54.874984741210938, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 9 + + ID + 43 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs20 \cf0 version 1} + + + + Bounds + {{18.000001907348633, 172.00001525878906}, {54.874984741210938, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 9 + + ID + 42 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs20 \cf0 version 2} + + + + Bounds + {{18.000001907348633, 132.00001525878906}, {54.874984741210938, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 9 + + ID + 41 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs20 \cf0 version 3} + + + + Class + LineGraphic + ID + 39 + Points + + {367.56781394720099, 96.934765010838973} + {340.87498664855957, 121.99999535646094} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 38 + + + + Bounds + {{236.62497329711914, 70}, {290.49996948242188, 27}} + Class + ShapedGraphic + ID + 38 + Shape + Circle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs28 \cf0 combination rule for apply function} + + + + Bounds + {{423.37497407197952, 121.99999535646094}, {37, 140}} + Class + ShapedGraphic + ID + 37 + Shape + Circle + Style + + fill + + Draws + NO + + shadow + + Draws + NO + + stroke + + CornerRadius + 27 + Pattern + 1 + + + + + Bounds + {{319.874988342655, 121.95213619171162}, {37, 140}} + Class + ShapedGraphic + ID + 36 + Line + + ID + 20 + Position + 0.53669750690460205 + RotationType + 0 + + Shape + Circle + Style + + fill + + Draws + NO + + shadow + + Draws + NO + + stroke + + CornerRadius + 27 + Pattern + 1 + + + + + Bounds + {{453.12497329711914, 292}, {83, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 14 + + HFlip + YES + ID + 35 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs28 \cf0 variable\ +(version 1)} + + + + Bounds + {{347.62497329711914, 292}, {83, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 14 + + HFlip + YES + ID + 34 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs28 \cf0 function\ +(version 3)} + + + + Bounds + {{469.62497329711914, 212}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 14 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 x} + + + + Bounds + {{258.62497329711914, 212}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 11 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 f} + + + + Bounds + {{364.12497329711914, 212}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 8 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 g} + + + + Bounds + {{68.624973297119141, 292}, {103, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 14 + + ID + 33 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs28 \cf0 result\ +(version 3)} + + + + Bounds + {{236.62497329711914, 292}, {83, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 14 + + HFlip + YES + ID + 30 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs28 \cf0 function\ +(version 2)} + + + + Bounds + {{68.624973297119141, 252}, {451, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 24 + + ID + 26 + Shape + Rectangle + Style + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural + +\f0\fs48 \cf0 y = f ( g ( x ) )} + + Wrap + NO + + + Class + LineGraphic + Head + + ID + 14 + + ID + 24 + Points + + {414.62497329711914, 232.00001436225315} + {469.12497329711914, 232.00001436225315} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 8 + + + + Class + LineGraphic + Head + + ID + 14 + + ID + 23 + Points + + {414.59249740134356, 201.65593330965854} + {469.15744919289472, 222.34406669034144} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 7 + + + + Class + LineGraphic + Head + + ID + 14 + + ID + 22 + Points + + {414.52338161271501, 171.25945654263191} + {469.22656498152327, 212.74054345736806} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 6 + + + + Class + LineGraphic + Head + + ID + 8 + + ID + 21 + Points + + {309.12497329711914, 232.00001623872726} + {363.62497329711914, 232.00001623872726} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 11 + + + + Class + LineGraphic + Head + + ID + 7 + + ID + 20 + Points + + {309.12497310611434, 191.97770727366566} + {363.62497517476532, 191.93006203286416} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 10 + + + + Class + LineGraphic + Head + + ID + 6 + + ID + 19 + Points + + {309.09249740134356, 182.34406669034144} + {363.65744919289472, 161.65593330965854} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 10 + + + + Class + LineGraphic + Head + + ID + 10 + + ID + 18 + Points + + {172.1136803707216, 163.24080152942756} + {212.62497329711914, 172} + {258.14370307128587, 184.82217740117372} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 3 + + + + Class + LineGraphic + Head + + ID + 10 + + ID + 17 + Points + + {172.12497329711914, 192.00001953595211} + {258.12497329711914, 192.00001953595211} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 4 + + + + Class + LineGraphic + Head + + ID + 11 + + ID + 16 + Points + + {172.12497329711914, 232.0000196276261} + {258.12497329711914, 232.0000196276261} + + Style + + stroke + + HeadArrow + 0 + Legacy + + LineType + 1 + TailArrow + 0 + + + Tail + + ID + 5 + + + + Bounds + {{258.62497329711914, 172}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 10 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 f'} + + + + Bounds + {{364.12497329711914, 172}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 12 + + ID + 7 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 g'} + + + + Bounds + {{364.12497329711914, 132}, {50, 40}} + Class + ShapedGraphic + FontInfo + + Font + Helvetica + Size + 18 + + ID + 6 + Shape + Rectangle + Style + + shadow + + Draws + NO + + + Text + + Text + {\rtf1\ansi\ansicpg1252\cocoartf1265\cocoasubrtf210 +\cocoascreenfonts1{\fonttbl\f0\fswiss\fcharset0 Helvetica;} +{\colortbl;\red255\green255\blue255;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc + +\f0\fs36 \cf0 g''} + + + + GridInfo + + GuidesLocked + NO + GuidesVisible + YES + HPages + 1 + ImageCounter + 1 + KeepToScale + + Layers + + + Lock + NO + Name + Layer 1 + Print + YES + View + YES + + + LayoutInfo + + Animate + NO + circoMinDist + 18 + circoSeparation + 0.0 + layoutEngine + dot + neatoSeparation + 0.0 + twopiSeparation + 0.0 + + LinksVisible + NO + MagnetsVisible + NO + MasterSheets + + ModificationDate + 2014-12-25 05:46:50 +0000 + Modifier + atton + NotesVisible + NO + Orientation + 2 + OriginVisible + NO + PageBreaks + YES + PrintInfo + + NSBottomMargin + + float + 41 + + NSHorizonalPagination + + coded + BAtzdHJlYW10eXBlZIHoA4QBQISEhAhOU051bWJlcgCEhAdOU1ZhbHVlAISECE5TT2JqZWN0AIWEASqEhAFxlwCG + + NSLeftMargin + + float + 18 + + NSPaperSize + + size + {594.99997329711914, 842} + + NSPrintReverseOrientation + + int + 0 + + NSRightMargin + + float + 18 + + NSTopMargin + + float + 18 + + + PrintOnePage + + ReadOnly + NO + RowAlign + 1 + RowSpacing + 36 + SheetTitle + Canvas 1 + SmartAlignmentGuidesActive + YES + SmartDistanceGuidesActive + YES + UniqueID + 1 + UseEntirePage + + VPages + 1 + WindowInfo + + CurrentSheet + 0 + ExpandedCanvases + + + name + Canvas 1 + + + Frame + {{373, 4}, {892, 874}} + ListView + + OutlineWidth + 142 + RightSidebar + + ShowRuler + + Sidebar + + SidebarWidth + 120 + VisibleRegion + {{-99, 0}, {757, 735}} + Zoom + 1 + ZoomValues + + + Canvas 1 + 1 + 1 + + + + + diff -r e233b786623e -r 9d0c57803ca0 figure/apply_function.pdf Binary file figure/apply_function.pdf has changed diff -r e233b786623e -r 9d0c57803ca0 figure/apply_function.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/figure/apply_function.xbb Thu Dec 25 14:52:33 2014 +0900 @@ -0,0 +1,8 @@ +%%Title: ./apply_function.pdf +%%Creator: extractbb 20130405 +%%BoundingBox: 0 0 538 280 +%%HiResBoundingBox: 0.000000 0.000000 538.000000 280.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Thu Dec 25 14:47:27 2014 + diff -r e233b786623e -r 9d0c57803ca0 sigse.pdf Binary file sigse.pdf has changed diff -r e233b786623e -r 9d0c57803ca0 sigse.tex --- a/sigse.tex Thu Dec 25 14:05:51 2014 +0900 +++ b/sigse.tex Thu Dec 25 14:52:33 2014 +0900 @@ -38,7 +38,7 @@ Shinji Kono\affiref{ie-ryukyu}} \begin{abstract} -大学の講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづきと，それらに基づいた形式手法を広めるための意見を述べます。 +大学の講義や卒業研究を通して形式手法を学んだ一年ほどの過程やつまづき，それらに基づいた形式手法を広めるための意見を述べます． \end{abstract} % 表題などの出力 @@ -67,9 +67,20 @@ Delta を用いたプログラムでは，変数は必ず Delta で記述し，関数は必ず Delta を返すようにします．プログラムへの変更は，関数か変数のバージョンアップとして表現し，Delta への新しい値の追加として記述します．そうすることにより，任意の変数もしくは関数は必ず1つ以上のバージョンを持ちます． + 次にバージョンを持った関数の適用を考えます． -関数の適用は通常の関数の適用と違い，変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません． -例えば，バージョンが3つある変数に対してバージョンが2つある関数を適用する場合，結果の変数のバージョンは2つにするか3つにするか決める必要があります． +関数の適用は変数と関数のバージョンの違いを考慮したルールに基づいて適用しなくてはなりません． +例えば，バージョンが1つある変数に対してバージョンが3つある関数と2つある関数を適用する場合，結果の変数のバージョンがいくつになるか決めなくては適用することができません(図\ref{apply_function})． + +\begin{figure}[htbp] + \begin{center} + \includegraphics[scale=0.4]{./figure/apply_function.pdf} + \caption{関数適用時のバージョンの組み合せ例} + \label{apply_function} + \end{center} +\end{figure} + + 変数と関数のバージョンの組み合せのルールは Monad を用いて記述しました． Haskell における Monad はデータ構造とメタな計算との対応付けです\cite{moggi}．メタ計算としてバージョンの組み合せの解決を $ \mu $ と $ \eta $ により定義します．