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.
The page introduces syntax and semantics of erlc
Syntax and Typing
A erlc code is a list of erlc statements. A elrc statement is either one of the three:
- 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
check t; checks if the term
t is welltyped and prints the type of
eval[n, m] t; evaluates the term
t in working precision
n and prints the result using
m decimals. Note:
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
The syntax of erlc term looks almost alike typed lambda calculus’s. Hence, erlc types are composed of base types and higher types:
- base types :=
REAL | NAT | BOOL | UNIT
- higher types :=
type -> type | type * type
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 :=
- projection :=
- primitive constants :=
- user constants :=
- Variables :=
Type checking is done as anyone would suppose.
erlc offers the following primitive
- natural number arith.:=
+ * : NAT -> NAT -> NATinfix
- natural number comparison:=
> < = : NAT -> NAT -> BOOLinfix
- real number arith. :=
+. -. *. /. :REAL -> REAL -> REALinfix
- real number comparison :=
>. <. : REAL -> REAL -> BOOLinfix
- 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) -> UNITwhere
tis 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
tis 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
document under construction…