• 数学
  • 简介:一个自然科学及其衍生物的结构记录形式

  • @ 2022-4-3 13:28:20

项目地址

用该设计书写的自然数相关内容(节选)

"用皮亚诺规则定义的非负整数"
design 自然数<:Number
	zero(::Type)
	next(::this)
	=(::this,::this)::Bool
	初始值规则 : isa(zero(this),this)
	后继规则(n::this) : isa(next(n),this)
	前继规则(n::this) : ⇒(≠(n,zero(this)),∃(p,this,=(n,next(p))))
	唯一性规则(a::this,b::this) : ⇒(≠(a,b),≠(next(a),next(b)))
	相等规则 : n_and(自反性(=(::this,::this)),对称性(=(::this,::this)),传递性(=(::this,::this)))
	归纳规则(p::Function{Tuple{this},Bool}) : n_⇒(
		call(p,zero(this)),
		∀(n,this,⇒(call(p,n),call(p,next(n)))),
		恒等于(p,true)
	)
end
construct 自然数
	data::Set
	function zero(t::Type)
		if same(t,this)
			return new(∅)
		else
			@findnext
		end
	end
	next(n::this): this(∪(n.data,Set(n.data)))
	=(a::this,b::this): =(a.data,b.data)
	proof 初始值规则()
		same(this,this)						:c same_is_same this
		same(zero(this),callbranch(rough))	:@branch zero(this) [1]
		same(callbranch(rough),new(∅))		:@leaf callbranch(zero,this,`a`)
	same(zero(this),new(∅))				:a [3|1] [2|1]
		isa(new(∅),this)					:@calc_type new(∅)
		@QED								:a [5|1] [4|1]
	end
	proof 后继规则(n::this)
		isa(this(rough),this) 		:@calc_type this(∪(n.data,Set(n.data)))
		same(next(n),this(rough)) 	:@leaf next(n)
		@QED						:a [1|1] [2|1]
	end
	proof 前继规则(n::this)
		@QED :@jump
	end
	# todo
end
enviroment
	let Nat: 自然数
	let 0: zero(Nat)
	function one(t::Type)
		if same(t,Nat)
			return next(zero(Nat))
		else
			@findnext
		end
	end
	function prev(n::Nat)
		if same(n,0)
			return undefined
		else
			return 逆函数call(next,n)
		end
	end
	function +(a::Nat,b::Nat)
		if same(b,0)
			return a
		else
			return +(next(a),prev(b))
		end
	end
end
部分公理可能需要(在FOPL+ZFC的基础上)增加或移除
我没有写解释器、Core、Base或stdlib的计划

本设计仍有很大的改进空间,欢迎意见/异见/建议/贡献

1 comments

  • 1