Last active
April 21, 2021 01:37
-
-
Save maxkrieger/64e253819586ca3690daa816290cc02d to your computer and use it in GitHub Desktop.
gpt-3
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Here is the "set theory" language: | |
type Set | |
type Point | |
type Map | |
constructor Singleton : Point p -> Set | |
function Intersection : Set a * Set b -> Set | |
function Union : Set a * Set b -> Set | |
function Subtraction : Set a * Set b -> Set | |
function CartesianProduct : Set a * Set b -> Set | |
function Difference : Set a * Set b -> Set | |
function Subset : Set a * Set b -> Set | |
function AddPoint : Point p * Set s1 -> Set | |
predicate Not : Prop p1 | |
predicate From : Map f * Set domain * Set codomain | |
predicate Empty : Set s | |
predicate Intersecting : Set s1 * Set s2 | |
predicate IsSubset : Set s1 * Set s2 | |
predicate PointIn : Set s * Point p | |
predicate In : Point p * Set s | |
predicate Injection : Map m | |
predicate Surjection : Map m | |
predicate Bijection : Map m | |
predicate PairIn : Point * Point * Map | |
notation "A ⊂ B" ~ "IsSubset(A, B)" | |
notation "p ∈ A" ~ "PointIn(A, p)" | |
notation "p ∉ A" ~ "PointNotIn(A, p)" | |
notation "A ∩ B = ∅" ~ "Not(Intersecting(A, B))" | |
notation "f: A -> B" ~ "Map f; From(f, A, B)" | |
Here is an example of the "set theory" language: | |
Set A | |
Set B | |
Set C | |
Set D | |
Set E | |
Set F | |
Set G | |
IsSubset(B, A) | |
IsSubset(C, B) | |
IsSubset(D, C) | |
IsSubset(E, D) | |
IsSubset(F, E) | |
IsSubset(G, F) | |
--- | |
Here is the "linear algebra" language: | |
type Scalar | |
type VectorSpace | |
type Vector | |
type LinearMap | |
function neg: Vector v -> Vector | |
function scale: Scalar c * Vector v -> Vector cv | |
function addV: Vector * Vector -> Vector | |
function addS: Scalar s1 * Scalar s2 -> Scalar | |
function norm: Vector v -> Scalar | |
function innerProduct: Vector * Vector -> Scalar | |
function determinant: Vector * Vector -> Scalar | |
function apply: LinearMap f * Vector -> Vector | |
predicate In: Vector * VectorSpace V | |
predicate From: LinearMap V * VectorSpace domain * VectorSpace codomain | |
predicate Not: Prop p1 | |
predicate Orthogonal: Vector v1 * Vector v2 | |
predicate Independent: Vector v1 * Vector v2 | |
predicate Dependent: Vector v1 * Vector v2 | |
predicate Unit: Vector v | |
notation "det(v1, v2)" ~ "determinant(v1, v2)" | |
notation "LinearMap f : U → V" ~ "LinearMap f; From(f, U, V)" | |
notation "v1 + v2" ~ "addV(v1, v2)" | |
notation "-v1" ~ "neg(v1)" | |
notation "Vector a ∈ U" ~ "Vector a; In(a, U)" | |
notation "|y1|" ~ "norm(y1)" | |
notation "<v1,v2>" ~ "innerProduct(v1, v2)" | |
notation "s * v1" ~ "scale(s, v1)" | |
notation "Scalar c := " ~ "Scalar c; c := " | |
notation "f(v)" ~ "apply(f, v)" | |
Here is an example of the "linear algebra" language: | |
VectorSpace V |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
VectorSpace W | |
LinearMap f : V → W | |
Vector v1 := Vector(2, 1) | |
Vector v2 := Vector(3, 0) | |
Dependent(v1, v2) | |
Independent(v1, v2) | |
Orthogonal(v1, v2) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
slightly better result: