# erlc-js

Exact Real Lambda Calculus (** erlc**) is a simple functional language that offers real numbers as its abstract datatype. It can be thought as a functional variant of ERC language.

** erlc-js** is a javascript program that parses and runs a

**program.**

*erlc***development version can be found in my workspace**

*erlc-js*The page introduces syntax and semantics of *erlc*

## Syntax and Typing

### Statement

A ** erlc** code is a list of

**statements. A**

*erlc***statement is either one of the three:**

*elrc*- definition :=
`DEFINE ident := term ;`

- type checking :=
`CHECK term ;`

- evaluation :=
`EVAL[NUM, NUM] term ;`

CAPITALIZED words in the page represents tokens. `DEFINE`

is ‘define’, `CHECK`

is ‘check’ and `EVAL`

is ‘eval’. Like this, throughout the page, `S`

will be a token for the string ‘s’. `NUM`

is a token for positive integer numbers such as ‘0’, ‘1’, …

`define s := t;`

statement, when it succeeds, defines the term `t`

to have name `s`

.
`check t;`

checks if the term `t`

is welltyped and prints the type of `t`

.
`eval[n, m] t;`

evaluates the term `t`

in working precision `n`

and prints the result using `m`

decimals. Note: `n`

and `m`

are not ** erlc** terms that for example

`eval[3+4, 10+1] t;`

isn’t a correct statement.the parameters can be omitted that `eval t;`

will be `eval[52,10] t;`

.

### Types

The syntax of ** erlc** term looks almost alike typed lambda calculus’s. Hence,

**types are composed of base types and higher types:**

*erlc*- base types :=
`REAL | NAT | BOOL | UNIT`

- higher types :=
`type -> type | type * type`

### Terms

** erlc** explicitly has pairing and its projection as primitive

`term`

constructions. The reason is to make a notion of interval primitive in the language.- lambda abstraction :=
`\ ident : type . term`

- function application :=
`term @ term`

- pairing :=
`(term, term)`

- projection :=
`fst term`

and`snd term`

- primitive constants :=
`constant`

- user constants :=
`user_constant`

- Variables :=
`ident`

### Type Checking

Type checking is done as anyone would suppose.

### Constants

** erlc** offers the following primitive

`constants`

:- natural number arith.:=
`+ * : NAT -> NAT -> NAT`

infix - natural number comparison:=
`> < = : NAT -> NAT -> BOOL`

infix - real number arith. :=
`+. -. *. /. :REAL -> REAL -> REAL`

infix - real number comparison :=
`>. <. : REAL -> REAL -> BOOL`

infix - natural numbers :=
`NUM : NAT`

- real number from natural number :=
`INJ : NAT -> REAL`

- multivalued select :=
`SELECT : UNIT -> UNIT-> BOOL`

- lower and upperbound of a real function on an interval :=
`MOD : (REAL -> REAL) -> REAL -> REAL -> (REAL * REAL)`

- limit :=
`LIM : (NAT -> REAL) -> REAL`

- definedness of any type :=
`DOWN(t) -> UNIT`

where`t`

is any type. - primitive recursion :=
`REC_UNIT(t) : t -> UNIT -> t`

`REC_BOOL(t) : t -> t -> BOOL -> t`

`REC_NAT(t) : t -> (NAT -> t -> t) -> (NAT -> t)`

where`t`

is any type.

### User Constants and variable Scoping

When an identifier `s`

is defiend using `DEFINE s := t;`

statement, `s`

will be used as `user_constant`

in all terms constructed after the statement. Variable scoping works as it does not matter what variables are used inside the statement.
For example, when `DEFINE f := \x:real. x +. INJ 10;`

is done and the definition is used latter as `\x:real. f @ x`

, it will automatically be translated to `\x:real. (\x':real. x' +. INJ 10);`

### Implicitly typed arguments

** erlc** being a typed lambda calculus and forbidding general polymorphism, indeed all lambda bindings should have explicit types.

However, it is so annoying to do so! Hence, ** erlc-js** has its own type inferring engine that when it is obvious what type should a variable have, it is okay not to specify the variable’s type. But this depends on the power of the type inference system of

**.**

*erlc-js*With the type inferring of ** erlc-js**,

`\x. t`

is also a well-formed term of lambda abstraction. If **says**

*erlc-js*`x`

should have type `tp`

, the term `\x. t`

will be parsed to `x:tp. t`

.## Semantics

document under construction…