spring-raining/index.html

## index.html
<!DOCTYPE html>
<html>
  <head>
      <meta charset="utf-8" />
      <title>Markdown to HTML</title>
<script type="text/x-mathjax-config">
  MathJax.Hub.Config({
    jax: ["input/TeX","output/HTML-CSS"],
    extensions: [],
    TeX: {
      extensions: ["AMSmath.js","AMSsymbols.js","noErrors.js","noUndefined.js"]
    },
    showMathMenu: false
  });
</script>
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js">
</script>
      <style>.markdown-preview:not([data-use-github-style]) { padding: 2em; font-size: 1.2em; color: rgb(248, 248, 242); overflow: auto; background-color: rgb(40, 40, 40); }
.markdown-preview:not([data-use-github-style]) > :first-child { margin-top: 0px; }
.markdown-preview:not([data-use-github-style]) h1, .markdown-preview:not([data-use-github-style]) h2, .markdown-preview:not([data-use-github-style]) h3, .markdown-preview:not([data-use-github-style]) h4, .markdown-preview:not([data-use-github-style]) h5, .markdown-preview:not([data-use-github-style]) h6 { line-height: 1.2; margin-top: 1.5em; margin-bottom: 0.5em; color: rgb(255, 255, 255); }
.markdown-preview:not([data-use-github-style]) h1 { font-size: 2.4em; font-weight: 300; }
.markdown-preview:not([data-use-github-style]) h2 { font-size: 1.8em; font-weight: 400; }
.markdown-preview:not([data-use-github-style]) h3 { font-size: 1.5em; font-weight: 500; }
.markdown-preview:not([data-use-github-style]) h4 { font-size: 1.2em; font-weight: 600; }
.markdown-preview:not([data-use-github-style]) h5 { font-size: 1.1em; font-weight: 600; }
.markdown-preview:not([data-use-github-style]) h6 { font-size: 1em; font-weight: 600; }
.markdown-preview:not([data-use-github-style]) strong { color: rgb(255, 255, 255); }
.markdown-preview:not([data-use-github-style]) del { color: rgb(219, 219, 189); }
.markdown-preview:not([data-use-github-style]) a, .markdown-preview:not([data-use-github-style]) a code { color: rgb(248, 248, 240); }
.markdown-preview:not([data-use-github-style]) img { max-width: 100%; }
.markdown-preview:not([data-use-github-style]) > p { margin-top: 0px; margin-bottom: 1.5em; }
.markdown-preview:not([data-use-github-style]) > ul, .markdown-preview:not([data-use-github-style]) > ol { margin-bottom: 1.5em; }
.markdown-preview:not([data-use-github-style]) blockquote { margin: 1.5em 0px; font-size: inherit; color: rgb(219, 219, 189); border-color: rgb(81, 81, 81); border-width: 4px; }
.markdown-preview:not([data-use-github-style]) hr { margin: 3em 0px; border-top-width: 2px; border-top-style: dashed; border-top-color: rgb(81, 81, 81); background: none; }
.markdown-preview:not([data-use-github-style]) table { margin: 1.5em 0px; }
.markdown-preview:not([data-use-github-style]) th { color: rgb(255, 255, 255); }
.markdown-preview:not([data-use-github-style]) th, .markdown-preview:not([data-use-github-style]) td { padding: 0.66em 1em; border: 1px solid rgb(81, 81, 81); }
.markdown-preview:not([data-use-github-style]) pre, .markdown-preview:not([data-use-github-style]) code { color: rgb(255, 255, 255); background-color: rgb(60, 60, 60); }
.markdown-preview:not([data-use-github-style]) pre, .markdown-preview:not([data-use-github-style]) pre.editor-colors { margin: 1.5em 0px; padding: 1em; font-size: 0.92em; border-radius: 3px; background-color: rgb(50, 50, 50); }
.markdown-preview:not([data-use-github-style]) kbd { color: rgb(255, 255, 255); border-width: 1px 1px 2px; border-style: solid; border-color: rgb(81, 81, 81) rgb(81, 81, 81) rgb(66, 66, 66); background-color: rgb(60, 60, 60); }
.markdown-preview[data-use-github-style] { font-family: 'Helvetica Neue', Helvetica, 'Segoe UI', Arial, freesans, sans-serif; line-height: 1.6; word-wrap: break-word; padding: 30px; font-size: 16px; color: rgb(51, 51, 51); overflow: scroll; background-color: rgb(255, 255, 255); }
.markdown-preview[data-use-github-style] > :first-child { margin-top: 0px !important; }
.markdown-preview[data-use-github-style] > :last-child { margin-bottom: 0px !important; }
.markdown-preview[data-use-github-style] a:not([href]) { color: inherit; text-decoration: none; }
.markdown-preview[data-use-github-style] .absent { color: rgb(204, 0, 0); }
.markdown-preview[data-use-github-style] .anchor { position: absolute; top: 0px; left: 0px; display: block; padding-right: 6px; padding-left: 30px; margin-left: -30px; }
.markdown-preview[data-use-github-style] .anchor:focus { outline: none; }
.markdown-preview[data-use-github-style] h1, .markdown-preview[data-use-github-style] h2, .markdown-preview[data-use-github-style] h3, .markdown-preview[data-use-github-style] h4, .markdown-preview[data-use-github-style] h5, .markdown-preview[data-use-github-style] h6 { position: relative; margin-top: 1em; margin-bottom: 16px; font-weight: bold; line-height: 1.4; }
.markdown-preview[data-use-github-style] h1 .octicon-link, .markdown-preview[data-use-github-style] h2 .octicon-link, .markdown-preview[data-use-github-style] h3 .octicon-link, .markdown-preview[data-use-github-style] h4 .octicon-link, .markdown-preview[data-use-github-style] h5 .octicon-link, .markdown-preview[data-use-github-style] h6 .octicon-link { display: none; color: rgb(0, 0, 0); vertical-align: middle; }
.markdown-preview[data-use-github-style] h1:hover .anchor, .markdown-preview[data-use-github-style] h2:hover .anchor, .markdown-preview[data-use-github-style] h3:hover .anchor, .markdown-preview[data-use-github-style] h4:hover .anchor, .markdown-preview[data-use-github-style] h5:hover .anchor, .markdown-preview[data-use-github-style] h6:hover .anchor { padding-left: 8px; margin-left: -30px; text-decoration: none; }
.markdown-preview[data-use-github-style] h1:hover .anchor .octicon-link, .markdown-preview[data-use-github-style] h2:hover .anchor .octicon-link, .markdown-preview[data-use-github-style] h3:hover .anchor .octicon-link, .markdown-preview[data-use-github-style] h4:hover .anchor .octicon-link, .markdown-preview[data-use-github-style] h5:hover .anchor .octicon-link, .markdown-preview[data-use-github-style] h6:hover .anchor .octicon-link { display: inline-block; }
.markdown-preview[data-use-github-style] h1 tt, .markdown-preview[data-use-github-style] h2 tt, .markdown-preview[data-use-github-style] h3 tt, .markdown-preview[data-use-github-style] h4 tt, .markdown-preview[data-use-github-style] h5 tt, .markdown-preview[data-use-github-style] h6 tt, .markdown-preview[data-use-github-style] h1 code, .markdown-preview[data-use-github-style] h2 code, .markdown-preview[data-use-github-style] h3 code, .markdown-preview[data-use-github-style] h4 code, .markdown-preview[data-use-github-style] h5 code, .markdown-preview[data-use-github-style] h6 code { font-size: inherit; }
.markdown-preview[data-use-github-style] h1 { padding-bottom: 0.3em; font-size: 2.25em; line-height: 1.2; border-bottom-width: 1px; border-bottom-style: solid; border-bottom-color: rgb(238, 238, 238); }
.markdown-preview[data-use-github-style] h1 .anchor { line-height: 1; }
.markdown-preview[data-use-github-style] h2 { padding-bottom: 0.3em; font-size: 1.75em; line-height: 1.225; border-bottom-width: 1px; border-bottom-style: solid; border-bottom-color: rgb(238, 238, 238); }
.markdown-preview[data-use-github-style] h2 .anchor { line-height: 1; }
.markdown-preview[data-use-github-style] h3 { font-size: 1.5em; line-height: 1.43; }
.markdown-preview[data-use-github-style] h3 .anchor { line-height: 1.2; }
.markdown-preview[data-use-github-style] h4 { font-size: 1.25em; }
.markdown-preview[data-use-github-style] h4 .anchor { line-height: 1.2; }
.markdown-preview[data-use-github-style] h5 { font-size: 1em; }
.markdown-preview[data-use-github-style] h5 .anchor { line-height: 1.1; }
.markdown-preview[data-use-github-style] h6 { font-size: 1em; color: rgb(119, 119, 119); }
.markdown-preview[data-use-github-style] h6 .anchor { line-height: 1.1; }
.markdown-preview[data-use-github-style] p, .markdown-preview[data-use-github-style] blockquote, .markdown-preview[data-use-github-style] ul, .markdown-preview[data-use-github-style] ol, .markdown-preview[data-use-github-style] dl, .markdown-preview[data-use-github-style] table, .markdown-preview[data-use-github-style] pre { margin-top: 0px; margin-bottom: 16px; }
.markdown-preview[data-use-github-style] hr { height: 4px; padding: 0px; margin: 16px 0px; border: 0px none; background-color: rgb(231, 231, 231); }
.markdown-preview[data-use-github-style] ul, .markdown-preview[data-use-github-style] ol { padding-left: 2em; }
.markdown-preview[data-use-github-style] ul.no-list, .markdown-preview[data-use-github-style] ol.no-list { padding: 0px; list-style-type: none; }
.markdown-preview[data-use-github-style] ul ul, .markdown-preview[data-use-github-style] ul ol, .markdown-preview[data-use-github-style] ol ol, .markdown-preview[data-use-github-style] ol ul { margin-top: 0px; margin-bottom: 0px; }
.markdown-preview[data-use-github-style] li > p { margin-top: 16px; }
.markdown-preview[data-use-github-style] dl { padding: 0px; }
.markdown-preview[data-use-github-style] dl dt { padding: 0px; margin-top: 16px; font-size: 1em; font-style: italic; font-weight: bold; }
.markdown-preview[data-use-github-style] dl dd { padding: 0px 16px; margin-bottom: 16px; }
.markdown-preview[data-use-github-style] blockquote { padding: 0px 15px; color: rgb(119, 119, 119); border-left-width: 4px; border-left-style: solid; border-left-color: rgb(221, 221, 221); }
.markdown-preview[data-use-github-style] blockquote > :first-child { margin-top: 0px; }
.markdown-preview[data-use-github-style] blockquote > :last-child { margin-bottom: 0px; }
.markdown-preview[data-use-github-style] table { display: block; width: 100%; overflow: auto; word-break: keep-all; }
.markdown-preview[data-use-github-style] table th { font-weight: bold; }
.markdown-preview[data-use-github-style] table th, .markdown-preview[data-use-github-style] table td { padding: 6px 13px; border: 1px solid rgb(221, 221, 221); }
.markdown-preview[data-use-github-style] table tr { border-top-width: 1px; border-top-style: solid; border-top-color: rgb(204, 204, 204); background-color: rgb(255, 255, 255); }
.markdown-preview[data-use-github-style] table tr:nth-child(2n) { background-color: rgb(248, 248, 248); }
.markdown-preview[data-use-github-style] img { max-width: 100%; box-sizing: border-box; }
.markdown-preview[data-use-github-style] .emoji { max-width: none; }
.markdown-preview[data-use-github-style] span.frame { display: block; overflow: hidden; }
.markdown-preview[data-use-github-style] span.frame > span { display: block; float: left; width: auto; padding: 7px; margin: 13px 0px 0px; overflow: hidden; border: 1px solid rgb(221, 221, 221); }
.markdown-preview[data-use-github-style] span.frame span img { display: block; float: left; }
.markdown-preview[data-use-github-style] span.frame span span { display: block; padding: 5px 0px 0px; clear: both; color: rgb(51, 51, 51); }
.markdown-preview[data-use-github-style] span.align-center { display: block; overflow: hidden; clear: both; }
.markdown-preview[data-use-github-style] span.align-center > span { display: block; margin: 13px auto 0px; overflow: hidden; text-align: center; }
.markdown-preview[data-use-github-style] span.align-center span img { margin: 0px auto; text-align: center; }
.markdown-preview[data-use-github-style] span.align-right { display: block; overflow: hidden; clear: both; }
.markdown-preview[data-use-github-style] span.align-right > span { display: block; margin: 13px 0px 0px; overflow: hidden; text-align: right; }
.markdown-preview[data-use-github-style] span.align-right span img { margin: 0px; text-align: right; }
.markdown-preview[data-use-github-style] span.float-left { display: block; float: left; margin-right: 13px; overflow: hidden; }
.markdown-preview[data-use-github-style] span.float-left span { margin: 13px 0px 0px; }
.markdown-preview[data-use-github-style] span.float-right { display: block; float: right; margin-left: 13px; overflow: hidden; }
.markdown-preview[data-use-github-style] span.float-right > span { display: block; margin: 13px auto 0px; overflow: hidden; text-align: right; }
.markdown-preview[data-use-github-style] code, .markdown-preview[data-use-github-style] tt { padding: 0.2em 0px; margin: 0px; font-size: 85%; border-radius: 3px; background-color: rgba(0, 0, 0, 0.0392157); }
.markdown-preview[data-use-github-style] code::before, .markdown-preview[data-use-github-style] tt::before, .markdown-preview[data-use-github-style] code::after, .markdown-preview[data-use-github-style] tt::after { letter-spacing: -0.2em; content: " "; }
.markdown-preview[data-use-github-style] code br, .markdown-preview[data-use-github-style] tt br { display: none; }
.markdown-preview[data-use-github-style] del code { text-decoration: inherit; }
.markdown-preview[data-use-github-style] pre > code { padding: 0px; margin: 0px; font-size: 100%; word-break: normal; white-space: pre; border: 0px; background: transparent; }
.markdown-preview[data-use-github-style] .highlight { margin-bottom: 16px; }
.markdown-preview[data-use-github-style] .highlight pre, .markdown-preview[data-use-github-style] pre { padding: 16px; overflow: auto; font-size: 85%; line-height: 1.45; border-radius: 3px; background-color: rgb(247, 247, 247); }
.markdown-preview[data-use-github-style] .highlight pre { margin-bottom: 0px; word-break: normal; }
.markdown-preview[data-use-github-style] pre { word-wrap: normal; }
.markdown-preview[data-use-github-style] pre code, .markdown-preview[data-use-github-style] pre tt { display: inline; max-width: initial; padding: 0px; margin: 0px; overflow: initial; line-height: inherit; word-wrap: normal; border: 0px; background-color: transparent; }
.markdown-preview[data-use-github-style] pre code::before, .markdown-preview[data-use-github-style] pre tt::before, .markdown-preview[data-use-github-style] pre code::after, .markdown-preview[data-use-github-style] pre tt::after { content: normal; }
.markdown-preview[data-use-github-style] kbd { display: inline-block; padding: 3px 5px; font-size: 11px; line-height: 10px; color: rgb(85, 85, 85); vertical-align: middle; border-style: solid; border-width: 1px; border-color: rgb(204, 204, 204) rgb(204, 204, 204) rgb(187, 187, 187); border-radius: 3px; box-shadow: rgb(187, 187, 187) 0px -1px 0px inset; background-color: rgb(252, 252, 252); }
.markdown-preview[data-use-github-style] a { color: rgb(51, 122, 183); }
.markdown-preview[data-use-github-style] pre, .markdown-preview[data-use-github-style] code { color: inherit; }
.markdown-preview[data-use-github-style] pre, .markdown-preview[data-use-github-style] pre.editor-colors { padding: 0.8em 1em; margin-bottom: 1em; font-size: 0.85em; border-radius: 4px; overflow: auto; }
.scrollbars-visible-always .markdown-preview pre.editor-colors::shadow .vertical-scrollbar, .scrollbars-visible-always .markdown-preview pre.editor-colors::shadow .horizontal-scrollbar { visibility: hidden; }
.scrollbars-visible-always .markdown-preview pre.editor-colors:hover::shadow .vertical-scrollbar, .scrollbars-visible-always .markdown-preview pre.editor-colors:hover::shadow .horizontal-scrollbar { visibility: visible; }
.markdown-preview del { text-decoration: none; position: relative; }
.markdown-preview del::after { border-bottom-width: 1px; border-bottom-style: solid; border-bottom-color: black; content: ""; left: 0px; position: absolute; right: 0px; top: 50%; }
.markdown-preview .flash { animation: flash 1s ease-out 1; outline: rgba(255, 0, 0, 0) solid 1px; }
.markdown-preview .flash:not(li) { display: block; }
.markdown-preview code { text-shadow: none; }
.bracket-matcher .region {
  border-bottom: 1px dotted lime;
  position: absolute;
}

.spell-check-misspelling .region {
  border-bottom: 2px dotted rgba(255, 51, 51, 0.75);
}

pre.editor-colors,
.host {
  background-color: #282828;
  color: #f8f8f2;
}
pre.editor-colors .invisible-character,
.host .invisible-character {
  color: rgba(197, 200, 198, 0.2);
}
pre.editor-colors .indent-guide,
.host .indent-guide {
  color: rgba(255, 255, 255, 0.15);
}
pre.editor-colors .wrap-guide,
.host .wrap-guide {
  background-color: rgba(255, 255, 255, 0.1);
}
pre.editor-colors .gutter,
.host .gutter {
  background-color: #303030;
}
pre.editor-colors .line-number.cursor-line-no-selection,
.host .line-number.cursor-line-no-selection {
  background-color: #49483e;
}
pre.editor-colors .invisible,
.host .invisible {
  color: #f8f8f2;
}
pre.editor-colors .cursor,
.host .cursor {
  border-color: #f8f8f0;
}
pre.editor-colors .selection .region,
.host .selection .region {
  background-color: #49483e;
}
pre.editor-colors .search-results .marker .region,
.host .search-results .marker .region {
  background-color: transparent;
  border: 1px solid #888888;
}
pre.editor-colors .search-results .marker.current-result .region,
.host .search-results .marker.current-result .region {
  border: 1px solid #ffffff;
}
pre.editor-colors .gfm .markup.heading,
.host .gfm .markup.heading {
  color: #a6e22e;
  font-weight: bold;
}
pre.editor-colors .gfm .markup.underline,
.host .gfm .markup.underline {
  color: #e6db74;
  text-decoration: underline;
}
pre.editor-colors .gfm .bold,
.host .gfm .bold {
  font-weight: bold;
}
pre.editor-colors .gfm .italic,
.host .gfm .italic {
  font-style: italic;
}
pre.editor-colors .gfm .raw,
.host .gfm .raw {
  color: #66d9ef;
}
pre.editor-colors .gfm .variable.list,
.host .gfm .variable.list {
  color: #f92672;
  font-weight: bold;
}
pre.editor-colors .gfm .link,
.host .gfm .link {
  color: #cccccc;
}
pre.editor-colors .gfm .link .entity,
.host .gfm .link .entity {
  color: #ae81ff;
}
.comment {
  color: #75715e;
}
.constant.character,
.constant.language,
.constant.numeric,
.constant.other {
  color: #ae81ff;
}
.entity.name.class {
  text-decoration: none;
  color: #a6e22e;
}
.entity.name.function {
  color: #a6e22e;
}
.entity.name.instance {
  color: #66d9ef;
}
.entity.name.tag {
  color: #f92672;
}
.entity.other.attribute-name {
  color: #a6e22e;
}
.entity.other.inherited-class {
  font-style: italic;
  text-decoration: none;
  color: #a6e22e;
}
.invalid {
  color: #f8f8f0;
  background-color: #f92672;
}
.invalid.deprecated {
  background-color: #ae81ff;
}
.keyword {
  color: #f92672 !important;
}
.meta.tag {
  color: #f8f8f2;
}
.storage {
  color: #f92672;
}
.storage.type {
  font-style: italic;
  color: #66d9ef;
}
.string {
  color: #e6db74;
}
.support.constant,
.support.function {
  color: #66d9ef;
}
.support.class,
.support.type {
  font-style: italic;
  color: #66d9ef;
}
.variable.parameter {
  font-style: italic;
  color: #fd971f;
}
.variable.language.python,
.variable.language.js {
  color: #f92672;
}
.class.jade {
  color: #ae81ff;
}
.leading-whitespace,
.trailing-whitespace {
  display: inline-block;
}
</style>
  </head>
  <body class='markdown-preview'><h1>9.4 対応関係の拡張</h1>
<h2>9.4.1 限量子と依存型</h2>
<h2>9.4.2 帰納と帰納型</h2>
<span class="math"><script type="math/tex; mode=display">\cfrac{Γ⊢A(0)　Γ,A(x)⊢A(x+1)}{Γ⊢∀x.(Nat(x)⊃A(x))}
</script></span>
<p><span class="math"><script type="math/tex">A(x)</script></span> について<span class="math"><script type="math/tex">A(0)</script></span> が成り立ち，<span class="math"><script type="math/tex">A(x)</script></span> が成り立つときに <span class="math"><script type="math/tex">A(x+1)</script></span> が成り立つなら，すべての自然数 <span class="math"><script type="math/tex">x</script></span> について <span class="math"><script type="math/tex">A(x)</script></span> が成り立つ．</p>
<p>このように帰納的に定義できる型を帰納型 <span class="math"><script type="math/tex">T</script></span> と呼ぶ．</p>
<p>たとえば，以下の <span class="math"><script type="math/tex">Nat</script></span>，<span class="math"><script type="math/tex">NatList</script></span> は帰納型である．</p>
<span class="math"><script type="math/tex; mode=display">\cfrac{}{Γ⊢0:Nat}　\cfrac{Γ⊢x:Nat}{Γ⊢s(x):Nat}
</script></span>
<span class="math"><script type="math/tex; mode=display">\cfrac{}{Γ⊢<>:NatList}　\cfrac{Γ⊢n:Nat　Γ⊢L:NatList}{Γ⊢<n,L>:NatList}
</script></span>
<p>数学的帰納法を計算体系によって表すと以下のようになる．</p>
<span class="math"><script type="math/tex; mode=display">\cfrac{Γ⊢n:Nat　Γ⊢f:Nat→T→T　Γ⊢a:T}{Γ⊢Rec(n,f,a):T}
</script></span>
<ul>
<li><span class="math"><script type="math/tex">n:Nat</script></span> は，帰納法の最初の根拠になる自然数．</li>
<li><span class="math"><script type="math/tex">a:T</script></span> は，<span class="math"><script type="math/tex">A(0)</script></span> の証拠に相当する（<span class="math"><script type="math/tex">A(0)</script></span> は <span class="math"><script type="math/tex">T</script></span> 型）．</li>
<li><span class="math"><script type="math/tex">f:Nat→T→T</script></span> は，<span class="math"><script type="math/tex">∀n:Nat(A(n)⊃A(n+1))</script></span> の証拠に相当する
（<span class="math"><script type="math/tex">A(n)</script></span> が <span class="math"><script type="math/tex">T</script></span> 型という証拠を受け取り，<span class="math"><script type="math/tex">A(n+1)</script></span> は <span class="math"><script type="math/tex">T</script></span> 型である証拠を返す関数）．</li>
</ul>
<p>ここで <span class="math"><script type="math/tex">Rec</script></span> 関数は以下のような計算規則を持つ．</p>
<span class="math"><script type="math/tex; mode=display">\begin{eqnarray*}
Rec(0,f,a) &→& a \\
Rec(s(n),f,a) &→& f(n,Rec(n,f,a))
\end{eqnarray*}
</script></span>
<p>上記の例では，<span class="math"><script type="math/tex">f</script></span> は単純に <span class="math"><script type="math/tex">n=0,1,2,…</script></span> の場合を計算するだけ（<span class="math"><script type="math/tex">f(x) = \verb| if | x=0 \verb| then | a \verb| else |f(x-1)</script></span>）で，これを原始帰納という．</p>
<p>これに対して，<span class="math"><script type="math/tex">f(x)</script></span> の中で <span class="math"><script type="math/tex">f(y)</script></span> で参照されるとき，<span class="math"><script type="math/tex">y</script></span> が <span class="math"><script type="math/tex">x</script></span> より前の値とは限らないような再帰を一般再帰という．</p>
<p>原始再帰は計算が必ず停止するが，一般再帰は必ずしも計算は停止しない．</p>
<h2>9.4.3 2階論理と多相型</h2>
<h2>9.4.4 古典理論とコントロールオペレータ</h2></body>
</html>