通讯技术>> symbolize>> 返回
项目作者： bsdz

项目描述 ：
Mathematical Symbol Engine
高级语言： Python
项目地址: git://github.com/bsdz/symbolize.git
创建时间： 2017-08-14T19:39:08Z
项目社区：https://github.com/bsdz/symbolize
开源协议：GNU General Public License v3.0
下载


symbolize

An attempt to implement symbolic math calculations and intuitionistic logic using Python.

Install

  1. python -m pip install git+https://github.com/bsdz/symbolize.git

Example

  1. from symbolize.logic.argument import Argument
  2. from symbolize.logic.typetheory.proposition import implies, ImpliesPropositionExpression, not_
  3. from symbolize.logic.typetheory.variables import A, B, C, Falsum
  5. A_implies_B = implies(A, B)
  6. B_implies_C = implies(B, C)
  7. a = A_implies_B.get_proof('a')
  8. b = B_implies_C.get_proof('b')
  9. x = A.get_proof('x')
  11. a

a : A \Rightarrow B

  1. b

b : B \Rightarrow C

  1. x

x : A

  1. arg1 = Argument([x, a], a(x))
  2. arg2 = Argument([arg1, b], b(arg1.conclusion))
  3. arg3 = Argument([arg2, x], arg2.conclusion.abstract(x))
  4. arg4 = Argument([arg2, x], arg3.conclusion.abstract(b))
  5. arg5 = Argument([arg2, x], arg4.conclusion.abstract(a))
  6. arg5

\frac{\frac{\frac{x : A \quad a : A \Rightarrow B}{a(x) : B} \quad b : B \Rightarrow C}{b(a(x)) : C} \quad x : A}{\lambda{}(a).\lambda{}(b).\lambda{}(x).(b(a(x))) : (A \Rightarrow B) \Rightarrow ((B \Rightarrow C) \Rightarrow (A \Rightarrow C))}

  1. new_type = arg5.conclusion.proposition_type.replace(C, Falsum).copy()
  2. new_type

(A \Rightarrow B) \Rightarrow ((B \Rightarrow \bot) \Rightarrow (A \Rightarrow \bot))

  1. new_type.walk(print)
  1. ExpressionWalkResult(expr: ⟹; obj: ⟹(⟹(A, B), ⟹(⟹(B, ⟘), ⟹(A, ⟘))); type: ImpliesPropositionSymbol)
  2. ExpressionWalkResult(expr: ⟹(A, B); obj: [⟹(A, B), ⟹(⟹(B, ⟘), ⟹(A, ⟘))][0]; type: ImpliesPropositionExpression; parent_type: ImpliesPropositionExpression)
  3. ExpressionWalkResult(expr: ⟹; obj: ⟹(A, B); type: ImpliesPropositionSymbol)
  4. ExpressionWalkResult(expr: A; obj: [A, B][0]; type: PropositionSymbol; parent_type: ImpliesPropositionExpression)
  5. ExpressionWalkResult(expr: B; obj: [A, B][1]; type: PropositionSymbol; parent_type: ImpliesPropositionExpression)
  6. ExpressionWalkResult(expr: ⟹(⟹(B, ⟘), ⟹(A, ⟘)); obj: [⟹(A, B), ⟹(⟹(B, ⟘), ⟹(A, ⟘))][1]; type: ImpliesPropositionExpression; parent_type: ImpliesPropositionExpression)
  7. ExpressionWalkResult(expr: ⟹; obj: ⟹(⟹(B, ⟘), ⟹(A, ⟘)); type: ImpliesPropositionSymbol)
  8. ExpressionWalkResult(expr: ⟹(B, ⟘); obj: [⟹(B, ⟘), ⟹(A, ⟘)][0]; type: ImpliesPropositionExpression; parent_type: ImpliesPropositionExpression)
  9. ExpressionWalkResult(expr: ⟹; obj: ⟹(B, ⟘); type: ImpliesPropositionSymbol)
  10. ExpressionWalkResult(expr: B; obj: [B, ⟘][0]; type: PropositionSymbol; parent_type: ImpliesPropositionExpression)
  11. ExpressionWalkResult(expr: ⟘; obj: [B, ⟘][1]; type: PropositionSymbol)
  12. ExpressionWalkResult(expr: ⟹(A, ⟘); obj: [⟹(B, ⟘), ⟹(A, ⟘)][1]; type: ImpliesPropositionExpression; parent_type: ImpliesPropositionExpression)
  13. ExpressionWalkResult(expr: ⟹; obj: ⟹(A, ⟘); type: ImpliesPropositionSymbol)
  14. ExpressionWalkResult(expr: A; obj: [A, ⟘][0]; type: PropositionSymbol; parent_type: ImpliesPropositionExpression)
  15. ExpressionWalkResult(expr: ⟘; obj: [A, ⟘][1]; type: PropositionSymbol)
  1. def my_sub(wr):
  2.     if type(wr.expr) is ImpliesPropositionExpression and wr.expr.base == implies and wr.expr.children[1] == Falsum:
  3.         wr.obj[wr.index] = not_(wr.expr.children[0])
  4. new_type.walk(my_sub)
  5. new_type

(A \Rightarrow B) \Rightarrow ((\neg(B)) \Rightarrow (\neg(A)))

  1. # switch off Tex render and render using unicode
  2. from symbolize.expressions import Expression
  3. Expression.jupyter_repr_html_function = lambda self: f"{self.repr_unicode()}"
  4. new_type

(A ⟹ B) ⟹ ((¬(B)) ⟹ (¬(A)))

For more examples see the Jupyter notebooks in the examples folder.

To Do

There is still lots to do initially implementing finite types and natural numbers. Further
into the project I would like to implement some simple symbolic manipulations and perhaps
even implement Gruntz (http://www.cybertester.com/data/gruntz.pdf)

References

  • [BN] Programming in Martin-Lofs Type Theory - Bengt Nordstrom
  • [ST] Type Theory & Functional Programming - Simon Thompson