In this paper we present the simply-typed Lambda calculus extended by typed arithmetic expressions, Boolean values, derived forms, and reference types. We brie y present its syntax and semantics. Based on that we construct a model of this language using category theory.
The simply-typed Lambda calculus is considered to be the simplest functional
programming language. It was introduced by the Alonzo Church and Stephen
Kleen [
In our previous research, we have worked with type theory and linear logic [
-calculus and T-NBL De nition
-calculus with The typed Number Boolean Language (T-NBL) is the base
language of this paper. As the basic sets of typed expressions of the -calculus are
considered the sets of natural numbers Nat and boolean values Bool [
T ::= Bool j Nat
De nition of simple typed -calculus with functional-type and with typed
Number Boolean Language (T-NBL) is composed of semantics and syntax [
= (T ; F )
T NBL + k = (
T = fBool; N at; T g ;
FT NBL + K = f
true; f alse :! Bool;
0 :! N at;
succ : N at ! N at;
pred : N at ! N at;
iszero : N at ! Bool;
if : Bool; T; T ! T;
x :! T;
abs : T ! T;
app : (T ! T ); T ! T; g)
Model of algebraic speci cation is characterized by [
f : T1; : : : ; Tn ! T0 Jf K : JT1K : : :
JTnK ! J T0K: Categorical model is created in the way that, to every name of basic types (Nat or Bool) is assigned a set of real types (N or B) and also to the operation speci cation, for example, to the pred is assigned a real operation JpredK. Real operation works with semantic domens, on which is arity de ned by cartesian product.
Categorical model consists of objects and morphisms. Objects are considered as semantical domens N, B, nal object 0, and the initial object f*g. Morphisms are composed of operations as follows:
Operation iszero is used for veri cation of zero value, is represented as
The conditional operation if is represented as morphism
(B + N) (B + N) ! B + N: { the morphisms of the -calculus: x : f*g ! B + N morphism for expression of variable.
J K JabsK : (B + N) ! (B + N) morphism for expression of abstraction. JappK : (B + N)(B + N) (B + N) ! (B + N) morphism for expression of application.
Model contains coprojections 1, 2 and projections 1, 2, '1, '2, '3.
The gure 1 shows categorical model of the T-NBL (purple color) with the -calculus (orange color). { the morphisms of the T-NBL language:
Jtrue=falseK : f*g ! B de nes the constants true or false. 0 : f*g ! N de nes the constant 0.
J K Operations successor and predecessor are represented in the model as (7) (8) (9) (10) (11) 3
Some of the programming languages have side e ects, for that reason derived
forms are used [
{ T = fBool; Nat; Unit; T g, { F = fseq; wild; asc; letg.
T ::= : : : j Unit
Syntax is extended by these alternatives [
Signature of derived forms consists of following:
Categorical model of derived forms consists of objects, with these semantic domens N, B, U, nal object 0, and initial object f*g. Morphisms consists of operations of derived forms as follows: { Operation sequence is represented as morphism JseqK : (U (B + N + U)) !
B + N + U. { Wildcards are de ned as JwildK : B + N + U ! B + N + U. { Ascription represents morphism JascK : f g ! B + N + U, { Let binding is JletK : ((B + N + U) (B + N + U)) ! B + N + U. Model contains coprojections 1, 2, 3 and projections 1, 2, '1, '2.
Corresponding categorical model of derived forms is depicted in the gure 2.
In the previous sections we have mentioned just pure elements, but most
programming languages contains also inpure elements. That is the reason for some
of the side e ects, and for that referentions are used. Referention determines a
value, that contains an adress of another value. Reference types are types, that
use just as much memory, as much is needed for the calculation. The basic
operations of reference types are alloc, dereference and assign. We add a reference
type to the basic sets of typed expressions [
Syntax is extended by these alternatives [
T ::= : : : j Ref t ::= : : : j ref t j !t j t := t; (13) where the rst alternative is alloc (ref), the second is dereference (!) and the last one represents assign (:=).
Signature of reference types consists of: { T = fBool; Nat; Unit; Ref; T g, { F = fref; !; :=g.
Ref = ( T = fBool; N at; U nit; T g ; FREF = f ref : T ! Ref T; ! : Ref T ! T; := : (Ref T T ) ! U nit; g) (15)
Categorical model of reference types is composed of objects [14], [15], where belong these semantic domens N, B, R, U, nal object 0, and beginning object f*g. Morphisms contains following operations: { alloc JrefK : (B + N + R + U) ! R (B + N + R + U), { dereference J!K : R (B + N + R + U) ! B + N + R + U, { assign J:=K : (B + N + R + U) (R (B + N + R + U)) ! U. Model contains coprojections 1, 2, 3, 4 and projections 1, 2, '1, '2. The corresponding categorical model of reference type is depicted in the gure 3. In this paper, we introduce the simply typed -calculus extended by T-NBL, derived forms and reference type.
Basic sets of typed expressions are as follows:
T ::= Bool j Natj Refj Unit: The syntax of our language is expressed by the following BNF production rule: t ::= true j false j if t then t else t j 0 j succ t j pred t j iszero t j (t) j x j x : T: t j t t j j ref t j !t j t := t j j ( x : Unit:t)t j ( : T:x)t j t as T j ( x : T:t):
Signature of extended simply typed -calculus contains: { T = fBool; Nat; Unit; Ref; T g, { F = funion of sets FT NBL; F K; FREF a FDSg:
Where:
FT NBL = ftrue; false; 0; succ; pred; iszero; ifg, F K = fx; abs; appg, FREF = fref; !; :=g,
FOT = fseq; wild; asc; letg.
+T NBL+OT +Ref = ( T = fBool; N at; U nit; T g ; F = f true; f alse :! Bool; 0 :! N at; succ : N at ! N at; pred : N at ! N at; iszero : N at ! Bool; if : Bool; T; T ! T; x : ! T; abs : T ! T; app : (T ! T ); T ! T; ref : T ! Ref T; ! : Re:f(RTef!TTT;) ! U nit; := seq : U nit; T ! T; wild : T ! T; asc :! T; let : T; T ! T g) (16) (17) (18)
The categorical model of typed -calculus extended by T-NBL, reference and derived forms was created by merging of the categorical models from past sections. It also contains following { coprojections 1, 2, 3, 4, and { projections 1, 2, 3, '1, '2, 1, 2, 1, 2, 1, 2, "1, "2.
Categorical model is depicted in the next gure 4, where the separated extensions are represented by di erent colors. Purple is for the extension of T-NBL, orange stands for -calculus, green is for reference and blue represents the extension of derived forms.
In this paper, we have introduced the simply typed -calculus extended by TNBL, derived forms, and reference types. The main result is a uni ed syntax, signature, algebraic model, and categorical model of simply typed -calculus extended by T-NBL, reference types, and derived forms. Final categorical model contains all the extensions of the simply typed -calculus, they are separated by di erent colors for better transparency of the model.
This work was supported by the following projects: { Faculty of Electrical Engineering and Informatics, Technical University of Kosice under the contract No. FEI-2018-59: Semantic Machine of SourceOriented Transparent Intensional Logic. { Slovak Research and Development Agency under the contract No. SK-AT2017-0012: Semantics technologies for computer science education. 13. V. Novitzka and D. Mihalyi, \Polymorphic type theory as a base for categorical logic," Acta Electrotechnica et Informatica No, vol. 7, no. 1, p. 3, 2007. 14. T. Hagino, \A typed lambda calculus with categorical type constructors," in Category theory and computer science. Springer, 1987, pp. 140{157. 15. L. Vokorokos, A. Balaz, and M. Chovanec, \Distributed detection system of security intrusions based on partially ordered events and patterns," in Towards Intelligent Engineering and Information Technology. Springer, 2009, pp. 389{403.