caotic123/Ane-Language

---

caotic123/Ane-Language.json

{
  "createdAt": "2019-01-06T02:30:43Z",
  "defaultBranch": "master",
  "description": "A tool for analyze lambda calculus terms",
  "fullName": "caotic123/Ane-Language",
  "homepage": "",
  "language": "Haskell",
  "name": "Ane-Language",
  "pushedAt": "2019-01-14T16:30:29Z",
  "stargazersCount": 6,
  "topics": [],
  "updatedAt": "2022-06-04T16:05:59Z",
  "url": "https://github.com/caotic123/Ane-Language"
}

Ane-Language

Ane is a tool-language to analyze lambda terms that’s ensure a real time manipulation of lambda terms. Ane uses total untyped lambda calculus, however you can use typed operations therefore terms can be easily changed and makes assumptions.

A non-recursive pair example :

Definition : pair.
Term pair : λx -> λy -> λf -> λencapsule -> ((f x) y).
End_Terms.

Reducible pair.
Type of pair is (* -> (* -> ((* -> (* -> *)) -> (* -> *)))).

Beta-Reduction pair in x in λp -> *.
Beta-Reduction pair in y in λp -> (* *).

Apply pair.
Finish as [λx -> λy -> x : (λx -> λp -> *)]
          [λx -> λy -> y : (λy -> λp -> (* *))].
End_Definition.

Or you need to know if two terms computes in the same way:

Simply Example ::
Definition : ret.
Term ret : λx -> λi -> x.
Term retTwo : λx -> λi -> ((λx -> x) x).
Term Atom : λatom -> *.
End_Terms.

Beta-Reduction ret in x in Atom.
Beta-Reduction retTwo in x in Atom.
Apply ret.
Apply retTwo.
Equal ret and retTwo.
Show.
Finish as : λi -> (λatom -> *).
End_Definition.

Operations

Apply in Term : Linear walk in a lambda function in a term and evaluates aplications
Term a : λx -> ((λf -> f) *), change the Term for
Term a : λx -> x

Equal Term and Term : Compare two functions lambda through a identy function lambda
Term one = λx -> x
Term two = λy -> x
Equal one two.

Finish Term as : Y : Seems like equal, but it's applicable in main term and compare any (Term/Lambda).
Finish Term as [X : y] [Y : z] ..., A matching [X, y] that apply X and compare if result is y.

Reducible X : Check if a term can be reduciable, therefore don't have any unknow free variable:
Term y : λx -> (x a)
Reducible y : Error (a isn't know)

ApplyTerms X : Substitue the terms of other terms.
Term y : λy -> x
Term x : λf -> λd -> d
ApplyTerms y = λy -> λf -> λd

Beta-Reduction X in Y in Z : Do a beta-reduction in a term.
Term x : λy -> λx -> (y *)
Beta-Reduction x in y in (λy -> y) =  λx -> ((λy -> y) *)

Type X of Y : Check if a Lambda Type X matching with a type Y
Term x : λy -> x
Type x of (* -> *) : Right

Show : Just Show the lambda functions

Normalization of Term strongly by Y : Uses strongly normalization to reduce a lambda term
Normalization of Any strongly by (* -> (* - > *)) = if any is Type (* -> (* - > *)), so can be applicable to a minimal term.

BetaExpasion Term in X in Y :
Yet not implemented

Recursion of Term in Y : Yet not implemented

Why Ane? Ane is a cool name

If need contact anything just text me : camposferreiratiago@gmail.com