2,619
次編輯
「型別理論與形式證明筆記」修訂間的差異
跳至導覽
跳至搜尋
無編輯摘要
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 104： | 行 104： | ||
# context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空） | # context（上下文）是一系列不同主體（不同變數）的宣告列表（註：context可為空） | ||
# judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement | # judgement（判斷）形如<math display="inline">\Gamma \vdash M:\sigma</math>，其中左邊的<math display="inline">\Gamma</math>是上下文，右邊的<math display="inline">M:\sigma</math>是statement | ||
==附註：本書使用的排版法== | |||
原本的書使用的排版法如下，類似[https://en.wikipedia.org/wiki/Fitch_notation Fitch的表示法(Fitch notation)]，雖然可以用HTML硬畫，但是很不好當筆記使用： | |||
<div> | |||
<table style="margin-bottom:1em;"> | |||
<tr> | |||
<td style="border:1px solid black;padding:0.5em;">假設A</td></tr><tr> | |||
<td style="border-left:1px solid black; padding:1em;" ><table style="margin-bottom:0.5em;"> | |||
<tr> | |||
<td style="border:1px solid black;padding:0.5em;">假設B</td></tr><tr> | |||
<td style="border-left:1px solid black; padding:1em;" >C</td> | |||
</tr><tr> | |||
<td style="border-left:1px solid black; padding:1em;" >⋮</td> | |||
</tr><tr><td>D</td></tr> | |||
</table></td> | |||
</tr><tr><td>E</td></tr> | |||
</table> | |||
</div> | |||
所以姑且改編Fitch表示法，變如下： | |||
<pre> | |||
(a) *A* | |||
(b) | *B* | |||
(1) | | C | |||
| | ⋮ | |||
(n) | | D | |||
(n+1) | E | |||
</pre> | |||
[[category:資訊]] | [[category:資訊]] | ||