![自然数 + 加法 - 型
sealed trait 自然数 {
def +( n: 自然数 ) : 自然数
}
object 零 extends 自然数 {
def +( a: 自然数 ): 自然数 = a
}
case class 後者(b: 自然数) extends
自然数 {
def +( a: 自然数 ): 自然数 =
後者( a + b )
}
sealed trait 自然数 {
type 足す[N <: 自然数] <: 自然数
}
trait 零 extends 自然数{
override type 足す[N <: 自然数] = N
}
trait 後者[N<:自然数] extends 自然数
{
override type 足す[O <: 自然数] =
後者[N#足す[O]]
}](https://image.slidesharecdn.com/scala-160319061646/85/Scala-10-320.jpg)
![応用例 - N次元ベクトル
sealed trait ベクトル集合[次元 <: 自然数] {
def +( vector: ベクトル集合[次元] ): ベクトル集合[次元]
def append[Size <: 自然数]( vector: ベクトル集合[Size] ): ベク
トル集合[次元#足す[Size]]
}
https://github.
com/buster84/Natural/blob/master/src/main/scala/com/github/buster84/ベクトル.
scala](https://image.slidesharecdn.com/scala-160319061646/85/Scala-11-320.jpg)
![Riemann球面に 内接する直方体[第四回日曜数学会]](https://cdn.slidesharecdn.com/ss_thumbnails/sundaymath2anogif-160203122718-thumbnail.jpg?width=560&fit=bounds)
More Related Content
Viewers also liked (15)
実践厂肠补濒补て?ヘ?アノの公理
- 2. Who? ● 教育学部数学科 出身 ● @busterdayo ● https://jp.linkedin.com/in/yasuki-okumura-8561b32a ● サーバーサイドエンジニア at Tamecco
- 3. Agenda ● ペアノの公理 ● 自然数 - オブジェクト ● 自然数 + 加法 - オブジェクト ● 自然数 + 加法 - 型 ● 応用例 - N次元ベクトル
- 4. ペアノの公理 - wikipedia調べ 自然数は次の5条件を満たす。 ● 自然数 0 が存在する。 ● 任意の自然数 a にはその後者 (successor)、suc(a) が存在する（suc(a) は a + 1 の "意味"）。 ● 0 はいかなる自然数の後者でもない（0 より前の自然数は存在しない）。 ● 異なる自然数は異なる後者を持つ：a ≠ b のとき suc(a) ≠ suc(b) となる。 ● 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満 たすとき、すべての自然数はその性質を満たす。 https://ja.wikipedia.org/wiki/ペアノの公理
- 5. 自然数 - オブジェクト sealed trait 自然数 object 零 extends 自然数 case class 後者(a: 自然数) extends 自然数
- 6. scala> val 壱 = 後者(零) 壱: com.github.buster84.後者 = 後者(com.github.buster84.零$@4161bf5f) scala> val 弐 = 後者(壱) 弐: com.github.buster84.後者 = 後者(後者(com.github.buster84.零$@4161bf5f)) scala> val 参 = 後者(弐) 参: com.github.buster84.後者 = 後者(後者(後者(com.github.buster84.零$@4161bf5f))) scala> val 肆 = 後者(参) 肆: com.github.buster84.後者 = 後者(後者(後者(後者(com.github.buster84.零$@4161bf5f)))) scala> 壱 != 弐 res0: Boolean = true scala> 参 != 肆 res1: Boolean = true
- 7. 自然数 + 加法 - オブジェクト 自然数の加法は再帰的に、以下のように定義できる。 ● すべての自然数 a に対して、a + 0 = a ● すべての自然数 a, b に対して、a + suc(b) = suc(a + b) https://ja.wikipedia.org/wiki/自然数 ● すべての自然数 a に対して、零 + a = a ● すべての自然数 a, b に対して、後者(b) + a = 後者(a + b)
- 8. 自然数 + 加法 - オブジェクト sealed trait 自然数 { def +( n: 自然数 ) : 自然数 } object 零 extends 自然数 { def +( a: 自然数 ): 自然数 = a // 零 + a = a } case class 後者(b: 自然数) extends 自然数 { def +( a: 自然数 ): 自然数 = 後者( a + b ) // 後者(b) + a = 後者(a + b) }
- 9. scala> val 壱 = 後者(零) scala> val 弐 = 後者(壱) scala> val 参 = 後者(弐) scala> val 肆 = 後者(参) scala> 壱 + 壱 == 弐 res0: Boolean = true scala> 壱 + 壱 + 壱 == 参 res1: Boolean = true scala> 弐 + 弐 == 肆 res2: Boolean = true
- 10. 自然数 + 加法 - 型 sealed trait 自然数 { def +( n: 自然数 ) : 自然数 } object 零 extends 自然数 { def +( a: 自然数 ): 自然数 = a } case class 後者(b: 自然数) extends 自然数 { def +( a: 自然数 ): 自然数 = 後者( a + b ) } sealed trait 自然数 { type 足す[N <: 自然数] <: 自然数 } trait 零 extends 自然数{ override type 足す[N <: 自然数] = N } trait 後者[N<:自然数] extends 自然数 { override type 足す[O <: 自然数] = 後者[N#足す[O]] }
- 11. 応用例 - N次元ベクトル sealed trait ベクトル集合[次元 <: 自然数] { def +( vector: ベクトル集合[次元] ): ベクトル集合[次元] def append[Size <: 自然数]( vector: ベクトル集合[Size] ): ベク トル集合[次元#足す[Size]] } https://github. com/buster84/Natural/blob/master/src/main/scala/com/github/buster84/ベクトル. scala
- 12. デモ