Search results
Jump to navigation
Jump to search
Page title matches
- ...ic type theory underlying the [[wikipedia:Agda (programming language)|Agda programming language]]. UTT<sub>Σ</sub> differs from the calculus of constructions in three primary ways. ...2 KB (232 words) - 09:37, 12 November 2023
- ...pes. It is a bare-bones model of computation, based entirely on the notion of functions. It is Turing complete. ...typed λ-calculus (henceforth just λ-calculus), functions are the only form of data. Functions take functions as arguments, and return functions. The func ...14 KB (2,273 words) - 09:37, 12 November 2023
- ...means the same as the type <code>a -> a</code> in Haskell or ML. The piece of syntax <math>\forall \alpha</math> is called a "type quantifier." ...t we have just mentioned (namely, Turing incompleteness and undecidability of type checking). It is an implicitly typed, polymorphic type system which is ...11 KB (1,726 words) - 09:35, 12 November 2023
- ...age:Lambda_cube.png|frame|The λ-cube. Direction of each arrow is direction of inclusion. ]] The λ-cube is a set of eight type theories which combine three different type system features in a ...20 KB (3,327 words) - 23:31, 23 January 2025
- ...of the λ-cube. They generalize them by relaxing restrictions on the number of sorts, and the rules governing the sorts. ...Type}_1</math>. They had <math>(s_1,s_2)</math> rules which said how types of different sorts could be used to form function types. ...9 KB (1,433 words) - 17:53, 17 December 2022
- The simply typed λ-calculus is a [[Foundations of Functional Programming/Typed λ-calculi|typed λ-calculus]] with a monomorphic type system. It comes ...ressions. We use <math>\mathbf{A} \to \mathbf{B}</math> to denote the type of functions from <math>\mathbf{A}</math> to <math>\mathbf{B}</math>. ...22 KB (3,644 words) - 09:37, 12 November 2023
- ...of the information for the calculi we discuss, followed by an explanation of each property featured in the table. | Calculus of constructions (λPω) ...9 KB (1,229 words) - 09:35, 12 November 2023
Page text matches
- ...ic type theory underlying the [[wikipedia:Agda (programming language)|Agda programming language]]. UTT<sub>Σ</sub> differs from the calculus of constructions in three primary ways. ...2 KB (232 words) - 09:37, 12 November 2023
- ...years, quantum mechanics preceded classical physics. For a didactic point of view, it has changed. ...oncepts of Classical Statistical Mechanics|Introduction and Basic Concepts of Classical Statistical Mechanics]] ...3 KB (477 words) - 19:16, 29 September 2016
- The simply typed λ-calculus is a [[Foundations of Functional Programming/Typed λ-calculi|typed λ-calculus]] with a monomorphic type system. It comes ...ressions. We use <math>\mathbf{A} \to \mathbf{B}</math> to denote the type of functions from <math>\mathbf{A}</math> to <math>\mathbf{B}</math>. ...22 KB (3,644 words) - 09:37, 12 November 2023
- ...age:Lambda_cube.png|frame|The λ-cube. Direction of each arrow is direction of inclusion. ]] The λ-cube is a set of eight type theories which combine three different type system features in a ...20 KB (3,327 words) - 23:31, 23 January 2025
- ...pes. It is a bare-bones model of computation, based entirely on the notion of functions. It is Turing complete. ...typed λ-calculus (henceforth just λ-calculus), functions are the only form of data. Functions take functions as arguments, and return functions. The func ...14 KB (2,273 words) - 09:37, 12 November 2023
- ...inguished from, though closely related to, its study from the perspectives of abstract algebra on the one hand and formal logic on the other. Two definitions of the relation concept are common in the literature. Although it is usually ...24 KB (3,641 words) - 07:51, 23 March 2023
- ==Bibliography for mathematical physics foundations== ...ries''' {http://planetphysics.us/encyclopedia/Cod.html} in the foundations of physics} ...55 KB (8,200 words) - 14:11, 6 May 2023
- Alfsen, E.M. and F. W. Schultz: \emph{Geometry of State Spaces of Operator Algebras}, Birkhauser, Boston--Basel--Berlin (2003). ...Butz, C., 2000, Topological Completeness for Higher Order Logic., Journal of Symbolic Logic, 65, 3, 1168--1182. ...64 KB (9,619 words) - 14:11, 6 May 2023
- ...be comprehensive, list of relevant, selected references for several areas of both abstract and applied mathematics. A more extensive bibliography on [[. ...//plato.stanford.edu/entries/category-theory/ Plato, Stanford Encyclopedia of Philosophy web site on category theory and its applications]. ...65 KB (9,661 words) - 04:57, 12 September 2020
- ...be comprehensive, list of relevant, selected references for several areas of both abstract and applied mathematics. A more extensive bibliography on cat ...//plato.stanford.edu/entries/category-theory/ Plato, Stanford Encyclopedia of Philosophy web site]. ...66 KB (9,841 words) - 12:46, 6 May 2023
- ...be comprehensive, list of relevant, selected references for several areas of both abstract and applied mathematics. A more extensive bibliography on [[. ...//plato.stanford.edu/entries/category-theory/ Plato, Stanford Encyclopedia of Philosophy web site]. ...66 KB (9,854 words) - 12:46, 6 May 2023
- ...resents a connection from the output of one artificial neuron to the input of another.]] ...justs as learning proceeds. The weight increases or decreases the strength of the signal at a connection. Neurons may have a threshold such that a signal ...82 KB (11,244 words) - 17:40, 29 December 2024
- ...error correction]] is a specific type of error correction code. It is one of the oldest but it is still widely used, as it is very well defined and seve ...codes are interesting applications to study, as they have the specificity of displaying visually the error correction code, rendering these codes readil ...101 KB (15,785 words) - 10:42, 20 October 2024