Ideals, Varieties, and Algorithms Exercises 1.2

2. let \mathcal{F}_2 be the field from Exercise 1.

  • a. Consider the polynomial g(x,y) = x^2 y + y^2 x \in \mathcal{F}_2 [x,y]. Show that g(x,y)=0 for every (x,y) \in \mathcal{F}^2_2, and explain why this does not contradict Proposition 5.
  • b. Find a nonzero polynomial in \mathcal{F}_2[x,y,z] which vanishes at every point of \mathcal{F}^3_2. Try to find one involving all three variables.
  • c. Find a nonzero polynomial in \mathcal{F}_2[x_1, \dots ,x_n] which vanishes at every point of \mathcal{F}^3_2. Can you find one in which all of x_1, \dots ,x_n appear?
  • a.の解

\mathcal{F}_2 = \{ 0,1 \}と言ってるんだから、(x,y)のパターンとして(0,0),(0,1),(1,0),(1,1)をあてはめて具体的に計算する.g(x,y)の計算結果はいずれも0であることが分かる.

なんでこれが、Proposition 5と矛盾しないのか、というと、Proposition 5では infinite fieldを仮定するから.本問の\mathcal{F}_2はfinite fieldなので、矛盾ではない.

  • b.の解

一例として、g(x,y,z) = xyz + xyz がある.(x,y,z)に0,1いずれを入れても、g(x,y,z)は0.

  • c.の解

b.と同様。g(x_1, \dots ,x_n) = x_1 \dots x_n + x_1 \dots x_n.

「形式手法入門」のP22「2.1.3 抽象データの表現と解析」

Alloy

P25の「代数的な性質の検査」の4条件のうち、2と4はandじゃなくてimpliesになるのでは。

module Queue
abstract sig Node { next : lone Node }
abstract sig Queue { root : lone Node }

fact noCycle { no n : Node | n in n.^next }
fact noReflexive { no n : Node | n = n.next }
fact allNodeInAQueue {
	all n : Node | some q : Queue | n in q.root.*next
}

sig Stack extends Queue {}
fact hasBottom {
	all s : Stack | Bottom in (s.root).*next
}
sig Entry extends Node { value : Value - Empty }
fact entryHasNext {
	all e : Entry | one e.next
}
sig Bottom extends Node {}
fact bottomDontHaveNext { no Bottom.next }

sig Value {}
one sig Empty extends Value {}

pred empty [s1 : Stack ] { s1.root = Bottom }

pred push [s1, s2 : Stack, v : Value ] {
	some e1 : Entry |
		e1.value = v && e1.next = s1.root && s2.root = e1
}

pred pop [ s1, s2 : Stack] {
	(s1.root = Bottom) => s2.root = s1.root
			      else s2.root = (s1.root).next
}

fun top [ s1 : Stack ] : Value {
	(s1.root = Bottom) => Empty else (s1.root).value
}

assert prop1 {
	all s1, s, s2 : Stack, v : Value |
		push[s1,s,v] and pop[s,s2] implies s1.root = s2.root
}

assert prop2 {
	all s1, s2 : Stack, v : Value |
		push[s1,s2,v] implies top[s2] = v
}

assert prop3 {
	all s1, s2 : Stack |
		empty[s1] and pop[s1,s2] implies s2.root = Bottom
}

assert prop4 {
	all s1 : Stack |
		empty[s1] implies top[s1] = Empty
}