東北大学 工学研究科 電気・情報系 2017年3月実施 専門科目 問題5 計算機2
Author
祭音Myyura (co-authored with GPT 5.6 SOL)
Description
日本語版
Fig. 5(a) の構文を持つプログラミング言語を考える。ただし、各式の意味は Fig. 5(b) の通りであるとする。たとえば、Fig. 5(c) で与えられるプログラムの下で式 は
のように評価される。また、このプログラムの下での の評価のように、プログラムの下での式の評価は停止しないことがある。
(1) Fig. 5(c) のプログラムについて以下の問に答えよ。
(a) このプログラムの下で および を評価せよ。評価の過程も示せ。
(b) 任意の自然数 と に対し、このプログラムの下で が に評価されることを数学的帰納法を用いて証明せよ。
(2) この言語におけるプログラミングに関する以下の問に答えよ。
(a) 自然数同士の乗算を行う関数 を含むプログラムを与えよ。
(b) 自然数 と の大小比較を行う関数 を含むプログラムを与えよ。ただし、このプログラムの下で は、 ならば に、そうでなければ に評価される。
(3) このプログラミング言語において、任意のプログラム とその中で定義される任意の 1 引数関数 に対し、各組に 1 つの自然数 を割り当てる単射が存在する。このとき、関数 を含むプログラム で次の性質を満たすものをこのプログラミング言語上で与えることはできない。
任意のプログラム とその中で定義される任意の 1 引数関数 および任意の自然数 について、プログラム の下で は、 の下で の評価が停止するときは に、そうでないときには に評価される。
このことを以下の手順に従い示せ。
- 上記のようなプログラム が存在することを仮定し、 に以下の関数を加えたプログラム を考えよ。
h(x) = ifz halt(x,x) then 0 else loop()
loop() = loop()
- の下で の評価が停止するか否かを議論せよ。
Fig. 5(a):
プログラム p ::= d1 ... dn
関数定義 d ::= f(x1,...,xn) = e
式 e ::= n
| succ(e)
| pred(e)
| x
| ifz e1 then e2 else e3
| f(e1,...,en)
Fig. 5(b):
| 式 | 意味 |
|---|---|
| 評価結果は となる。 | |
| を評価し、その結果を とする。すると全体の式の評価結果は となる。 | |
| を評価し、その結果を とする。そして、 であれば 、そうでなければ が全体の式の評価結果となる。 | |
ifz e1 then e2 else e3 | まず を評価する。その結果が であれば を評価し、そうでなければ を評価する。 |
| という関数定義が存在するものとする。まず (ただし )をそれぞれ評価し、その結果を とする。そして、関数 の本体である式 中の各 を自然数定数 で置き換えて得られる式を評価する。 |
Fig. 5(c):
f(x,y) = ifz x then y else succ(f(pred(x),y))
g(x) = g(x)
题目描述
程序由有限个函数定义 构成。表达式可为自然数常量、变量、succ(e)、pred(e)、ifz e1 then e2 else e3 或函数调用。succ 加一;pred(0)=0,否则减一;ifz 在条件等于零时只求值 then 分支,否则只求值 else 分支。函数调用先求全部实参,再以所得数值替换形参求函数体。
给定程序
f(x,y) = ifz x then y else succ(f(pred(x),y))
g(x) = g(x)
- (a) 求 的求值过程;(b) 用归纳法证明 。
- (a) 用此语言编写自然数乘法
mult;(b) 编写le(m,n),使其在 时输出 ,否则输出 。 - 每一对程序 及其中的一元函数 都有唯一自然数编码 。证明不存在此语言程序 中的函数
halt,能对所有 正确决定 是否终止(终止输出 ,否则输出 )。按要求向 添加
h(x) = ifz halt(x,x) then 0 else loop()
loop() = loop()
得到程序 ,讨论 的终止性。
Kai
(1)
固定 对 归纳: 时 ;若 ,则
故对任意 均成立,并且求值终止。
(2)
保留上述 ,增加
mult(m,n) = ifz m then 0 else f(n,mult(pred(m),n))
le(m,n) = ifz m then 1 else
(ifz n then 0 else le(pred(m),pred(n)))
乘法按第一个参数归纳即得 ;比较函数同时减一,直到一方为零,因此恰在 时返回 。
(3)
令 。若 halt(k,k)=0,其判定声称 不终止,但 立即返回 ;若 halt(k,k)=1,其判定声称 终止,但 执行 loop() 而不终止。两种情形均矛盾,故这样的 halt 不存在。