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 erlc program. erlc-js development version can be found in my workspace

The page introduces syntax and semantics of erlc

Syntax and Typing

Statement

A erlc code is a list of erlc statements. A elrc statement is either one of the three:

  1. definition := DEFINE ident := term ;
  2. type checking := CHECK term ;
  3. 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, erlc types are composed of base types and higher types:

  1. base types := REAL | NAT | BOOL | UNIT
  2. 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.

  1. lambda abstraction := \ ident : type . term
  2. function application := term @ term
  3. pairing := (term, term)
  4. projection := fst term and snd term
  5. primitive constants := constant
  6. user constants := user_constant
  7. Variables := ident

Type Checking

Type checking is done as anyone would suppose.

Constants

erlc offers the following primitive constants:

  1. natural number arith.:= + * : NAT -> NAT -> NAT infix
  2. natural number comparison:= > < = : NAT -> NAT -> BOOL infix
  3. real number arith. := +. -. *. /. :REAL -> REAL -> REAL infix
  4. real number comparison := >. <. : REAL -> REAL -> BOOL infix
  5. natural numbers := NUM : NAT
  6. real number from natural number := INJ : NAT -> REAL
  7. multivalued select := SELECT : UNIT -> UNIT-> BOOL
  8. lower and upperbound of a real function on an interval := MOD : (REAL -> REAL) -> REAL -> REAL -> (REAL * REAL)
  9. limit := LIM : (NAT -> REAL) -> REAL
  10. definedness of any type := DOWN(t) -> UNIT where t is any type.
  11. 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 erlc-js says x should have type tp, the term \x. t will be parsed to x:tp. t.

Semantics

document under construction…