Chess Engine Functions
>>Back to Sayulisp page
Contents
Constant Values
Squares
A1
: Number. It indicates A1 square. Value is '0'.
B1
: Number. It indicates B1 square. Value is '1'.
C1
: Number. It indicates C1 square. Value is '2'.
D1
: Number. It indicates D1 square. Value is '3'.
E1
: Number. It indicates E1 square. Value is '4'.
F1
: Number. It indicates F1 square. Value is '5'.
G1
: Number. It indicates G1 square. Value is '6'.
H1
: Number. It indicates H1 square. Value is '7'.
A2
: Number. It indicates A2 square. Value is '8'.
B2
: Number. It indicates B2 square. Value is '9'.
C2
: Number. It indicates C2 square. Value is '10'.
D2
: Number. It indicates D2 square. Value is '11'.
E2
: Number. It indicates E2 square. Value is '12'.
F2
: Number. It indicates F2 square. Value is '13'.
G2
: Number. It indicates G2 square. Value is '14'.
H2
: Number. It indicates H2 square. Value is '15'.
A3
: Number. It indicates A3 square. Value is '16'.
B3
: Number. It indicates B3 square. Value is '17'.
C3
: Number. It indicates C3 square. Value is '18'.
D3
: Number. It indicates D3 square. Value is '19'.
E3
: Number. It indicates E3 square. Value is '20'.
F3
: Number. It indicates F3 square. Value is '21'.
G3
: Number. It indicates G3 square. Value is '22'.
H3
: Number. It indicates H3 square. Value is '23'.
A4
: Number. It indicates A4 square. Value is '24'.
B4
: Number. It indicates B4 square. Value is '25'.
C4
: Number. It indicates C4 square. Value is '26'.
D4
: Number. It indicates D4 square. Value is '27'.
E4
: Number. It indicates E4 square. Value is '28'.
F4
: Number. It indicates F4 square. Value is '29'.
G4
: Number. It indicates G4 square. Value is '30'.
H4
: Number. It indicates H4 square. Value is '31'.
A5
: Number. It indicates A5 square. Value is '32'.
B5
: Number. It indicates B5 square. Value is '33'.
C5
: Number. It indicates C5 square. Value is '34'.
D5
: Number. It indicates D5 square. Value is '35'.
E5
: Number. It indicates E5 square. Value is '36'.
F5
: Number. It indicates F5 square. Value is '37'.
G5
: Number. It indicates G5 square. Value is '38'.
H5
: Number. It indicates H5 square. Value is '39'.
A6
: Number. It indicates A6 square. Value is '40'.
B6
: Number. It indicates B6 square. Value is '41'.
C6
: Number. It indicates C6 square. Value is '42'.
D6
: Number. It indicates D6 square. Value is '43'.
E6
: Number. It indicates E6 square. Value is '44'.
F6
: Number. It indicates F6 square. Value is '45'.
G6
: Number. It indicates G6 square. Value is '46'.
H6
: Number. It indicates H6 square. Value is '47'.
A7
: Number. It indicates A7 square. Value is '48'.
B7
: Number. It indicates B7 square. Value is '49'.
C7
: Number. It indicates C7 square. Value is '50'.
D7
: Number. It indicates D7 square. Value is '51'.
E7
: Number. It indicates E7 square. Value is '52'.
F7
: Number. It indicates F7 square. Value is '53'.
G7
: Number. It indicates G7 square. Value is '54'.
H7
: Number. It indicates H7 square. Value is '55'.
A8
: Number. It indicates A8 square. Value is '56'.
B8
: Number. It indicates B8 square. Value is '57'.
C8
: Number. It indicates C8 square. Value is '58'.
D8
: Number. It indicates D8 square. Value is '59'.
E8
: Number. It indicates E8 square. Value is '60'.
F8
: Number. It indicates F8 square. Value is '61'.
G8
: Number. It indicates G8 square. Value is '62'.
H8
: Number. It indicates H8 square. Value is '63'.
Fyles
FYLE_A
: Number. It indicates A-Fyle. Value is '0'.
FYLE_B
: Number. It indicates B-Fyle. Value is '1'.
FYLE_C
: Number. It indicates C-Fyle. Value is '2'.
FYLE_D
: Number. It indicates D-Fyle. Value is '3'.
FYLE_E
: Number. It indicates E-Fyle. Value is '4'.
FYLE_F
: Number. It indicates F-Fyle. Value is '5'.
FYLE_G
: Number. It indicates G-Fyle. Value is '6'.
FYLE_H
: Number. It indicates H-Fyle. Value is '7'.
Ranks
RANK_1
: Number. It indicates 1st rank. Value is '0'.
RANK_2
: Number. It indicates 2nd rank. Value is '1'.
RANK_3
: Number. It indicates 3rd rank. Value is '2'.
RANK_4
: Number. It indicates 4th rank. Value is '3'.
RANK_5
: Number. It indicates 5th rank. Value is '4'.
RANK_6
: Number. It indicates 6th rank. Value is '5'.
RANK_7
: Number. It indicates 7th rank. Value is '6'.
RANK_8
: Number. It indicates 8th rank. Value is '7'.
Sides
NO_SIDE
: Number. It indicates neither of sides. Value is '0'.
WHITE
: Number. It indicates White. Value is '1'.
BLACK
: Number. It indicates Black. Value is '2'.
Piece Types
EMPTY
: Number. It indicates no piece. Value is '0'.
PAWN
: Number. It indicates Pawn. Value is '1'.
KNIGHT
: Number. It indicates Knight. Value is '2'.
BISHOP
: Number. It indicates Bishop. Value is '3'.
ROOK
: Number. It indicates Rook. Value is '4'.
QUEEN
: Number. It indicates Queen. Value is '5'.
KING
: Number. It indicates King. Value is '6'.
Castling
NO_CASTLING
: Number. It indicates no one to castle. Value is '0'.
WHITE_SHORT_CASTLING
: Number.
It indicates White's Short Castling. Value is '1'.
WHITE_LONG_CASTLING
: Number.
It indicates White's Long Castling. Value is '2'.
BLACK_SHORT_CASTLING
: Number.
It indicates Black's Short Castling. Value is '3'.
BLACK_LONG_CASTLING
: Number.
It indicates Black's Long Castling. Value is '4'.
Engine Functions
gen-engine
Usage
(gen-engine)
((gen-engine) <Message Symbol> [<Arguments>...])
Description
- 1: Generates chess engine.
- 2: The engine executes something according to
<Message Symbol>
.
- 2: Some
<Message Symbol>
require <Argument>...
.
(help "engine <MessageSymbol>")
- Returns description for each message symbol.
Example
(define my-engine (gen-engine))
(display (my-engine '@get-white-pawn-position))
;; Output
;; > (A2 B2 C2 D2 E2 F2 G2 H2)
PGN Functions
gen-pgn
Usage
(gen-pgn <PGN string : String>)
Description
- Generates and returns PGN object from
<PGN string>
.
- PGN object is operated by Message Symbol.
- PGN object has 2 states.
- Current game.
- This can be changed by
@set-current-game
.
- Current move.
- This can be changed by
@next-move
, @prev-move
, @alt-move
,
@orig-move
, @rewind-move
.
Description of Message Symbols
-
@get-pgn-comments
- Returns Lists of comments about PGN.
-
@get-current-game-comments.
- Returns List of comments about the current game.
-
@get-current-move-comments
- Returns List of comments about the current move.
-
@length
- Returns the number of games that PGN has.
-
@set-current-game <Index : Number>
- Sets a current game into the
<Index>
th game.
-
@get-current-game-headers
- Returns List of Lists composed with headers of the current game.
- The format is "
((<Name 1> <value 1>) (<Name 2> <Value 2>)...)
".
-
@get-current-game-result
- Returns String of game result.
-
@current-move
- Returns the current move text.
- If there is no current move, it returns Nil.
-
@next-move
- Change the current move into the next move
and returns the move text.
- If there is no next move, it returns Nil.
-
@prev-move
- Change the current move into the previous move
and returns the move text.
- If there is no previous move, it returns Nil.
-
@alt-move
- Change the current move into the alternative move
and returns the move text.
- If there is no alternative move, it returns Nil.
-
@orig-move
- If the current move is an alternative move,
then change a current move into the original move
and returns the move text.
- If there is no original move, it returns Nil.
-
@rewind-move
- Change a current move into the first move
and returns the move text.
- If there is no first move, it returns Nil.
Example
;; Open PGN File.
(define pgn-file (input-stream "/path/to/pgnfile.pgn"))
;; Reads the file and generates PGN object.
(define my-pgn (gen-pgn (pgn-file '@read)))
;; Displays the current game headers.
(display (my-pgn '@get-current-game-headers))
;; Output
;; > (("Black" "Hanako Yamada") ("Site" "Japan")
;; > ("White" "Hironori Ishibashi"))
Utility Functions
sayuri-license
Usage
Description
- Returns String of license terms of Sayuri.
Example
(display (sayuri-license))
;; Output
;; > Copyright (c) 2013-2015 Hironori Ishibashi
;; >
;; > Permission is hereby granted, free of charge, to any person obtaining
;; > a copy
;; > of this software and associated documentation files (the "Software"),
;; > to
;; > deal in the Software without restriction, including without limitation
;; > the
;; > rights to use, copy, modify, merge, publish, distribute, sublicense,
;; > and/or
;; > sell copies of the Software, and to permit persons to whom the
;; > Software is
;; > furnished to do so, subject to the following conditions:
;; >
;; > The above copyright notice and this permission notice shall be
;; > included in
;; > all copies or substantial portions of the Software.
;; >
;; > THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
;; > EXPRESS OR
;; > IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
;; > MERCHANTABILITY,
;; > FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT
;; > SHALL THE
;; > AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
;; > LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
;; > ARISING
;; > FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
;; > DEALINGS IN THE SOFTWARE.
square->number
Usage
(square->number <Object>)
Description
- If
<Object>
is Square Symbol, it returns Number indicating to Square.
- If
<Object>
is List, it returns List changed Square Symbol into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (square->number symbol-list))
;; Output
;; > ((0 1 2)
;; > (FYLE_A FYLE_B FYLE_C)
;; > (RANK_1 RANK_2 RANK_3)
;; > (WHITE BLACK)
;; > (PAWN KNIGHT BISHOP)
;; > (WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
fyle->number
Usage
Description
- If
<Object>
is Fyle Symbol, it returns Number indicating to Fyle.
- If
<Object>
is List, it returns List changed Fyle Symbol into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (fyle->number symbol-list))
;; Output
;; > ((A1 B1 C1)
;; > (0 1 2)
;; > (RANK_1 RANK_2 RANK_3)
;; > (WHITE BLACK)
;; > (PAWN KNIGHT BISHOP)
;; > (WHITE_SHORT_CASTLING BLACK_LONG_CASTLING))
rank->number
Usage
Description
- If
<Object>
is Rank Symbol, it returns Number indicating to Rank.
- If
<Object>
is List, it returns List changed Rank Symbol into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (rank->number symbol-list))
;; Output
;; > ((A1 B1 C1)
;; > (FYLE_A FYLE_B FYLE_C)
;; > (0 1 2)
;; > (WHITE BLACK)
;; > (PAWN KNIGHT BISHOP)
;; > (WHITE_SHORT_CASTLING BLACK_LONG_CASTLING))
side->number
Usage
Description
- If
<Object>
is Side Symbol, it returns Number indicating to Side.
- If
<Object>
is List, it returns List changed Side Symbol into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (side->number symbol-list))
;; Output
;; > ((A1 B1 C1)
;; > (FYLE_A FYLE_B FYLE_C)
;; > (RANK_1 RANK_2 RANK_3)
;; > (1 2)
;; > (PAWN KNIGHT BISHOP)
;; > (WHITE_SHORT_CASTLING BLACK_LONG_CASTLING))
piece->number
Usage
Description
- If
<Object>
is Piece Type Symbol, it returns Number indicating
to Piece Type.
- If
<Object>
is List, it returns List changed Piece Type Symbol into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (piece->number symbol-list))
;; Output
;; > ((A1 B1 C1)
;; > (FYLE_A FYLE_B FYLE_C)
;; > (RANK_1 RANK_2 RANK_3)
;; > (WHITE BLACK)
;; > (1 2 3)
;; > (WHITE_SHORT_CASTLING BLACK_LONG_CASTLING))
castling->number
Usage
(castling->number <Object>)
Description
- If
<Object>
is Castling Right Symbol, it returns Number indicating
to Piece Type.
- If
<Object>
is List, it returns List changed Castling Right Symbol
into Number.
Example
(define symbol-list
'((A1 B1 C1)
(FYLE_A FYLE_B FYLE_C)
(RANK_1 RANK_2 RANK_3)
(WHITE BLACK)
(PAWN KNIGHT BISHOP)
(WHITE_SHORT_CASTLING BLACK_LONG_CASTLING)))
(display (castling->number symbol-list))
;; Output
;; > ((A1 B1 C1)
;; > (FYLE_A FYLE_B FYLE_C)
;; > (RANK_1 RANK_2 RANK_3)
;; > (WHITE BLACK)
;; > (PAWN KNIGHT BISHOP)
;; > (1 4))
chess->number
Usage
Description
- If
<Object>
is Symbol of Chess, it returns Number indicating
to Piece Type.
- If
<Object>
is List, it returns List changed Symbol of Chess
into Number.

- If
<Object>
is List, it returns List changed Number into Square Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->square number-list))
;; Output
;; > (A1 B1 C1 99)
number->fyle
Usage
Description
- If
<Object>
is Number, it returns Fyle Symbol.
- If
<Object>
is List, it returns List changed Number into Fyle Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->fyle number-list))
;; Output
;; > (FYLE_A FYLE_B FYLE_C 99)
number->rank
Usage
Description
- If
<Object>
is Number, it returns Rank Symbol.
- If
<Object>
is List, it returns List changed Number into Rank Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->rank number-list))
;; Output
;; > (RANK_1 RANK_2 RANK_3 99)
number->side
Usage
Description
- If
<Object>
is Number, it returns Side Symbol.
- If
<Object>
is List, it returns List changed Number into Side Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->side number-list))
;; Output
;; > (NO_SIDE WHITE BLACK 99)
number->piece
Usage
Description
- If
<Object>
is Number, it returns Piece Type Symbol.
- If
<Object>
is List, it returns List changed Number into Piece Type Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->piece number-list))
;; Output
;; > (EMPTY PAWN KNIGHT 99)
number->castling
Usage
(number->castling <Object>)
Description
- If
<Object>
is Number, it returns Castling Rights Symbol.
- If
<Object>
is List, it returns List changed Number
into Castling Rights Symbol.
Example
(define number-list '(0 1 2 99))
(display (number->castling number-list))
;; Output
;; > (NO_CASTLING WHITE_SHORT_CASTLING WHITE_LONG_CASTLING 99)
parse-fen/epd
Usage
(parse-fen/epd <FEN or EPD : String>)
Description
- Parses
<FEN or EPD>
and returns result value.
- A result value is
((<Tag 1 : String> <Object 1>)...)
.
Example
(display (parse-fen/epd
"rnbqkbnr/pp2pppp/3p4/2p5/3PP3/5N2/PPP2PPP/RNBQKB1R b KQkq d3 0 3"))
;; Output
;; > (("fen castling" (WHITE_SHORT_CASTLING
;; > WHITE_LONG_CASTLING BLACK_SHORT_CASTLING BLACK_LONG_CASTLING))
;; > ("fen clock" 0)
;; > ("fen en_passant" D3)
;; > ("fen ply" 5)
;; > ("fen position" ((WHITE ROOK) (WHITE KNIGHT) (WHITE BISHOP)
;; > (WHITE QUEEN) (WHITE KING) (WHITE BISHOP) (NO_SIDE EMPTY)
;; > (WHITE ROOK) (WHITE PAWN) (WHITE PAWN) (WHITE PAWN) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (WHITE PAWN) (WHITE PAWN) (WHITE PAWN)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (WHITE KNIGHT) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (WHITE PAWN)
;; > (WHITE PAWN) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (BLACK PAWN) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (BLACK PAWN)
;; > (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (BLACK PAWN) (BLACK PAWN) (NO_SIDE EMPTY) (NO_SIDE EMPTY)
;; > (BLACK PAWN) (BLACK PAWN) (BLACK PAWN) (BLACK PAWN) (BLACK ROOK)
;; > (BLACK KNIGHT) (BLACK BISHOP) (BLACK QUEEN) (BLACK KING)
;; > (BLACK BISHOP) (BLACK KNIGHT) (BLACK ROOK)))
;; > ("fen to_move" BLACK))
to-fen-position
Usage
(to-fen-position <Pieces list : List>)
Description
- Analyses
<Pieces list>
and returns FEN position.


Conversational Technologies
Speech Recognition Demo
with W3C Multimodal Standards
Speech Recognition
This demo uses the Web Speech API and creates EMMA documents from the results. You will need to use the Chrome browser.
Language
English
Chinese
French
German
Italian
Japanese
Portuguese
Spanish
Number of speech recognition results to return
Start Recognition
Stop Recognition
Speech recognition results:
Show MMI Event result
Clear Input
Event Log
Clear Events
Result


by Stephanie Yoon
Your input file must be a text-only PDF with a solid color background, and at least one pixel of space between lines.
White space is not included in the line count. There are some edge cases for which this app will output inaccurate results.
For more information, you can check out my GitHub repository.


Hey there,
Someone just submitted your form on {{host}}.Here's what they had to say:
| {{k}}: | {{data.get(k,'')|nl2br|safe}} |
You are receiving this because you confirmed this email address on {{config.SERVICE_NAME}}. If you don't remember doing that, or no longer wish to receive these emails, please remove the form on {{host}} or send an email to {{config.CONTACT_EMAIL}}.


Tabs Settings
Refresh content on clicking tab
Auto re-open previously viewed/opened tabs on reloading browser
Refresh content on tab when re-clicking the button or link


|
DATABASE TABLES - FPS |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 4 | 0 | No | - | Server ID. (e.g. 0001,0002) |
| NAME | C | 10 | 0 | No | - | Server name. (e.g. Server001, Server002) |
| DESCRIPTION | C | 50 | 0 | No | - | Server description. (e.g. HTTP Server, HTTPS Server) |
| IP | C | 48 | 0 | No | - | Server listenner IP address. (e.g. <IP_ADDRESS> to all IPs, <IP_ADDRESS> to bind to a specific IP) |
| PORT | N | 5 | 0 | No | - | Server listenner port number. (e.g. 80 to HTTP, 443 to HTTPS) |
| TYPE | C | 6 | 0 | No | - | Server type: HTTP - Hipertext Transfer Protocol FCGI - FastCGI Protocol TUNNEL - Tunnel Entry Points TUNNEX - Tunnel Exit Points |
| BANDWIDTH | N | 6 | 0 | No | - | HTTP bandwidth (kilobytes). |
| CHUNKED | N | 1 | 0 | No | - | Enables HTTP chunked transfer encoding: 0 - Disabled 1 - Enabled |
| COMPRESSION | N | 1 | 0 | No | - | Enables compression. (Used for TUNNEL and TUNNEX server types only) 0 - Disabled 1 - Enabled |
| KEEPALIVE | N | 1 | 0 | No | - | Enables HTTP connections keep alive: 0 - Disabled 1 - Enabled. |
| PASSWORD | C | 32 | 0 | No | - | Enables AES 256 encryption. Must be 32 bytes long. (Used for TUNNEL and TUNNEX server types only) |
| LOGLEVEL | N | 1 | 0 | No | - | Enables debug logging: 0 - Disabled 1 - Server events 2 - Server and threads events 3 - Server, threads and processing events. |
| LOGREQUESTS | N | 1 | 0 | No | - | Enables server requests logging: 0 - Disabled 1 - Enabled |
| REMOTEHOST | C | 50 | 0 | No | - | Remote host. (Used for TUNNEL and TUNNEX server types only) |
| REMOTEPORT | N | 5 | 0 | No | - | Remote port. (Used for TUNNEL and TUNNEX server types only) |
| SECURE | N | 1 | 0 | No | - | Enables secure connections (HTTPS): 0 - Disabled 1 - Enabled |
| CERTIFICATENAME | C | 50 | 0 | No | - | Certificate name or common name (CN). (e.g. www.example.com) |
| CERTIFICATESTORE | C | 50 | 0 | No | - | Certificate store or file name. |
| CERTIFICATEPASSWORD | C | 50 | 0 | No | - | Certificate file password. Used for certificate files stored in certificates folder. |
| STATE | N | 1 | 0 | No | - | Server state: 0 - Disabled 1 - Enabled |
| Label | Primary | Key |
| ID | Yes | ID |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 4 | 0 | No | - | Site ID. (e.g. 0001,0002) |
| SERVER | C | 4 | 0 | No | - | Server ID from SERVERS table. |
| NAME | C | 50 | 0 | No | - | Site name. (e.g. Site001, Site002) |
| DESCRIPTION | C | 50 | 0 | No | - | Site description. (e.g. PHPBB Forum, RoundCube Webmail) |
| HOSTNAME | C | 100 | 0 | No | - | The Host header received from HTTP request. (e.g. forum.example.com, webmail.example.com) |
| INDEX | C | 20 | 0 | No | - | Site index page. (e.g. index.fxp, index.php, index.html) |
| DIRECTORY | C | 100 | 0 | No | - | The full path to the folder that contains the site files. (e.g. c:\sites\phpbb, c:\sites\roundcube) |
| REDIRECT | C | 100 | 0 | No | - | The location to redirect (e.g. http://example.com, https://example.com) |
| Label | Primary | Key |
| ID | Yes | ID |
| SERVER | No | SERVER |
| HOSTNAME | No | HOSTNAME |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 4 | 0 | No | - | ID. (e.g. 0001, 0002) |
| SERVER | C | 4 | 0 | No | - | Server ID from SERVERS table. |
| NAME | C | 50 | 0 | No | - | Name. (e.g. Gateway001, Gateway002) |
| DESCRIPTION | C | 50 | 0 | No | - | Description. (e.g. FastCGI PHPBB Forum, FastCGI RoundCube Webmail) |
| HOSTNAME | C | 100 | 0 | No | - | The Host header received from HTTP request. (e.g. forum.example.com, webmail.example.com) |
| URI | C | 100 | 0 | No | - | The server will search the content of this field in the requested URI to determine when to send it to the gateway. (e.g. fill with ".php" to send every URI requests containing .php to the gateway) |
| PROTOCOL | C | 6 | 0 | No | - | Gateway protocol: FCGI - FastCGI |
| HOST | C | 50 | 0 | No | - | Remote host address or IP. |
| PORT | N | 5 | 0 | No | - | Remote port. |
| DIRECTORY | C | 100 | 0 | No | - | The full path to the folder that contains the site files. Should be the same of SITES table. (e.g. c:\sites\phpbb, c:\sites\roundcube) |
| Label | Primary | Key |
| ID | Yes | ID |
| SERVER | No | SERVER |
| URI | No | URI |
| HOSTNAME | No | HOSTNAME |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 8 | 0 | No | - | ID. (00000001, 00000002) |
| SITE | C | 4 | 0 | No | - | Site ID from SITES table. |
| REALM | C | 50 | 0 | No | - | Realm text sent to the client. |
| DIRECTORY | C | 100 | 0 | No | - | Realm directory. |
| TYPE | C | 6 | 0 | No | - | Realm type: Basic Digest |
| SUBFOLDERS | L | 1 | 0 | No | - | Apply to subfolders: 0 - No 1 - Yes |
| ASK | L | 1 | 0 | No | - | Ask for user password: 0 - No 1 - Yes |
| Label | Primary | Key |
| ID | Yes | ID |
| SITE | No | SITE |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 8 | 0 | No | - | User ID. |
| USERNAME | C | 50 | 0 | No | - | User name. |
| PASSWORD | C | 50 | 0 | No | - | User password. |
| Label | Primary | Key |
| ID | Yes | ID |
| USERNAME | No | USERNAME |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| REALM | C | 8 | 0 | No | - | Realm ID from REALMS table. |
| USER | C | 8 | 0 | No | - | User ID from USERS table. |
| Label | Primary | Key |
| USER | No | USER |
| REALM | No | REALM |
| Name | Type | Length | Decimals | Nulls | Default | Comments |
| ID | C | 8 | 0 | No | "" | CORS ID. (e.g. 00000001,00000002) |
| SITE | C | 4 | 0 | No | "" | Site ID from SITES table. |
| ORIGIN | C | 100 | 0 | No | "" | The Origin header received from HTTP request. (e.g. http://forum.example.com, http://webmail.example.com) |
| URI | C | 100 | 0 | No | "" | The resource identification. |
| GET | L | 1 | 0 | No | .F. | GET Method allowed. |
| POST | L | 1 | 0 | No | .F. | POST Method allowed. |
| PUT | L | 1 | 0 | No | .F. | PUT Method allowed. |
| DELETE | L | 1 | 0 | No | .F. | DELETE Method allowed. |
| HEAD | L | 1 | 0 | No | .F. | HEAD Method allowed. |
| OPTIONS | L | 1 | 0 | No | .F. | OPTIONS Method allowed. |
| HEADERS | M | 4 | 0 | No | "" | Allowed request headers. |
| Label | Primary | Key |
| ID | Yes | ID |
| SITE | No | SITE |
| URI | No | URI |
| ORIGIN | No | ORIGIN |


class Session extends Session
extends mfony\Component\HttpFoundation\Session\Session for adding some helpers
Class Session
Methods
| Lang|null |
getLang(bool $forceDefault = true)
|
|
|
setLang(Lang $lang)
|
||
|
setCurrency(Currency $currency)
|
||
| Currency |
getCurrency(bool $forceDefault = true)
Return current currency |
|
|
getAdminEditionCurrency()
|
||
|
setAdminEditionCurrency($currencyId)
|
||
|
getAdminEditionLang()
|
||
|
setAdminEditionLang($lang)
|
||
|
setCustomerUser(UserInterface $user)
|
||
|
getCustomerUser()
|
||
|
clearCustomerUser()
|
||
|
setAdminUser(UserInterface $user)
|
||
|
getAdminUser()
|
||
|
clearAdminUser()
|
||
|
setReturnToUrl($url)
|
||
| the |
getReturnToUrl()
|
|
| Cart|null |
getCart()
return cart if exists and is valid (checking customer) |
|
| $this |
setCart($cart_id $cart_id)
assign cart id in session |
|
|
setOrder(Order $order)
|
||
| Order |
getOrder()
|
|
| $this |
setProcessedOrder(Order $order)
|
|
| Order |
getProcessedOrder()
Return an order already processed, usefull for payment modules |
|
| $this |
setConsumedCoupons(array $couponsCode)
Set consumed coupons by the Customer |
|
| array |
getConsumedCoupons()
Get Customer consumed coupons |
Details
at line 51
public Lang|null
getLang(bool $forceDefault = true)
at line 61
public
setLang(Lang $lang)
at line 68
public
setCurrency(Currency $currency)
at line 80
public Currency
getCurrency(bool $forceDefault = true)
Return current currency
at line 93
public
getAdminEditionCurrency()
at line 104
public
setAdminEditionCurrency($currencyId)
at line 111
public
getAdminEditionLang()
at line 122
public
setAdminEditionLang($lang)
at line 131
public
setCustomerUser(UserInterface $user)
at line 138
public
getCustomerUser()
at line 143
public
clearCustomerUser()
at line 150
public
setAdminUser(UserInterface $user)
at line 157
public
getAdminUser()
at line 162
public
clearAdminUser()
at line 169
public
setReturnToUrl($url)
at line 180
public the
getReturnToUrl()
at line 192
public Cart|null
getCart()
return cart if exists and is valid (checking customer)
at line 232
public $this
setCart($cart_id $cart_id)
assign cart id in session
at line 241
public
setOrder(Order $order)
at line 251
public Order
getOrder()
at line 260
public $this
setProcessedOrder(Order $order)
at line 271
public Order
getProcessedOrder()
Return an order already processed, usefull for payment modules
at line 283
public $this
setConsumedCoupons(array $couponsCode)
Set consumed coupons by the Customer
at line 295
public array
getConsumedCoupons()
Get Customer consumed coupons


16 Boredom-Busting, Heart-Healthy Oatmeal Recipes
by Matthew Kadey, R.D.You may not know this, but oatmeal is one of Mother's Nature's favorite children. Why else would she bestow upon it the powers to help regulate diabetes , the fiber to assist in heart health , and the extra-special soluble fiber -glucan (seriously, that's not made up ).
One cup of cooked oatmeal contains four grams of fiber and only 166 calories. Fiber, as you may know, promotes heart and gut health and helps improve blood-sugar levels. If youre not eating enough fiber, oatmeal is a great place to start.
Yet despite Mother's Nature's preference for this near-holy whole grain, oatmeal is still, well, bland. Here's exactly how to cook oatmeal so that it has some texture and then 16 ways to elevate that oatmeal to bust breakfast boredom and wake up your morning bowl.
Step 1: Prep your base.
Skip instant oatmeal, which always turns soggy and soupy.
Instead, turn to steel-cut oats, which are hearty and soak up liquid while retaining their slight chew. Yes, they take longer to cook, but thats why its best to make them while you sleep.
In a medium-sized pot, add 2/3 cup steel-cut oats, a pinch of salt, and 1 3/4 cups water. Bring the water to a slight simmer (a few small bubbles breaking the surface) over medium heat, remove the pot from the heat, place a lid on it, and let the oats soak overnight.
Step 2: Add flavor.
In the morning, stir in a couple splashes of milk and any of the add-ins that follow. Then heat everything over medium low for 5 minutes, stirring a couple times. Transfer to a bowl and then apply your toppings. This makes enough for 2 servings.


We provide support for the following products: <<foreach [in products]>><<[IndexOf() != 0 ? ", " : ""]>><<[ProductName]>><</foreach>>


First name is required.
Last name is required.
Position/Title is required.
Email address is required.
Email address is invalid.
Password is required.
{{passwordError}}


This Bite is to illustrate scoping. You will sum numbers while keeping track of number of hundreds in a global variable called num_hundreds
.
To illustrate this see this REPL output:
>>> from scoping import sum_numbers, num_hundreds >>> num_hundreds -1 >>> sum_numbers([10, 20, 70]) 100 >>> from scoping import num_hundreds >>> num_hundreds 0 >>> sum_numbers([10, 120, 180]) 310 >>> from scoping import num_hundreds >>> num_hundreds 3
We planned to also illustrate nonlocal
, but we will do that in a separate Bite ... Good luck and keep calm and code in Python!


purpose: The purpose of this project will be a website that users can easily find restaurants around the Albuquerque area and see covid safety and ratings.
Audience:This site will be designed with an audience between the ages of 18-70 both male and female. Those who have underlying health issues that may be at risk, and also those who live with the elderly.
Goal: The primary goal for this site is to educate, connect, and provide covid statistics and safety for restaurants in the abq area
Profession: Works from home for a architecture firm. Has a wife and three kids. A little over weight and has an elderly mother who has diabetes and asthma. Enjoys Italian food and scary movies.
Technology: Macbook pro owner with 16 inch display. Iphone x with a verizon 5g connection. two ipads and a gaming PC
Attitudes & behaviors: spends long hours on the computer is not able to exercise as much as he would like. Does not eat a healthy diet and hardly ever gets sun light.
Frustrations and needs: needs to take preventive actions when leaving his home. Has an elderly mother that is high risk. with so much conflicting information he is not able to figure out where is safe to eat.
Goals: To be educated on different restaurants and their covid protocols. Be able to see the data for himself and review the ratings given to him so he can make the decision if the risk is worth it.
as a user, I need to be educated, understand safety protocols, and know the risks of eating at a restaurant


I have been a writer for a long time now. Supposedly, I’m quite good at it, if people are to be believed. “People” is really “my people,” though, and their praise generally feels biased to me. I’d like to be satisfied with my own work in the way that folks say I should be, but every time I read through something I’ve made, I end up scratching my head trying to figure out exactly where it fits in to writing at large. Classes in literature and rhetoric have been no help — they’ve always been more about reading than mapmaking, than placing different writing styles in context.
This project is an effort towards figuring out my own habits in reference to others. It is a data-driven study which compares a paper I wrote last year to assignments written by my roommates, Adam and Leah, as well as to a couple of books which I fished out of the used book sale that hit campus a few weeks ago. It doesn’t go too far, but it serves as a start to get people thinking about the ways in which writers sound distinct from each other. The metrics are an accessible balance between numbers one can wrap their head around and safe, color-coded passages. I’m quite pleased with those hues: they’re gentle and analogous, different enough to be distinguished, and particularly effective at encouraging readers to take in the entire document rather than losing themselves in close reading and missing the forest for the trees.
Rather than write an algorithm from scratch, I derived a lot of the statistics this document is built around using public, web-based tools. The names of these are in the bottom-right corner of the piece. Working around pre-existing systems with a lack of versatility was frustrating, and left me reeling from a handful of false starts. Nevertheless, I’m pleased to be able to say that the resources I used are all available to anybody who wants to take on this work and produce something that takes this idea even further.
Link to Project | MS Word Version of Introduction


class: center, middle # IEMS 5780
Building and Deploying Scalable
Machine Learning Services ### Lecture 5 - Recommender Systems #### Albert Au Yeung
4th October, 2019 --- class: middle, center # Recommender Systems --- # Agender ### Recommender Systems * Introduction * Content-based Recommendation Systems * Collaborative Filtering - User-based Neighbourhood Model - Item-based Neighbourhood Model - Matrix Factorization * Recommendation as Classification --- # Recommender Systems * We make a lot of **decisions** every day - Transportation - Restaurant reservation - Hotel reservation - Music - Movies * We usually rely on some **suggestions** or **recommendations** - Family and friends - Supervisors, teachers, seniors - Experts - The general public (word-of-mouth) --- # Recommender Systems ### What are the factors that affect our decisions? * Our own **preferences** (of the content, the characteristics, the price, etc.) * What do **most people like**? (which is the blockbuster movie recently?) * What do **people around us like**? (friends and family) * What do people **similar to us** like? --- # Example: Mobile App User Demographics
Ref: [You Are What Apps You Use: Demographic Prediction Based on User's Apps](https://arxiv.org/abs/1603.00059) --- # Example: Mobile App User Demographics
Ref: [You Are What Apps You Use: Demographic Prediction Based on User's Apps](https://arxiv.org/abs/1603.00059) --- # Recommender Systems * There are **many** items out there for us to choose - Tens of thousands of movies and songs - More than 1 million apps in the Android and iPhone app stores - Millions of books published every year * We need more efficient way to **filter information**, and identify items **most relevant** to us * On the other hand, producers also want to **provide consumers things that they really want** (targetted marketing) --- # Mobile Apps
([https://www.statista.com/statistics/266210/number-of-available-applications-in-the-google-play-store/](https://www.statista.com/statistics/266210/number-of-available-applications-in-the-google-play-store/)) --- # Movies
([https://stephenfollows.com/how-many-films-are-released-each-year/](https://stephenfollows.com/how-many-films-are-released-each-year/)) --- # Solution: Recommender Systems * Use **computers** and **algorithms** to process the huge amount of inforamtion and do the **filtering** for us * Analyse the **tastes** and **preferences** of different people * Analyse the **characteristics** of different items/products * Generate **personalized** recommendation based on users' **past activities** and **feedback** * Systems performing the above tasks are referred to as **recommender systems** / **recommendation systems** --- class: split # Examples of Recommender Systems .column-left[
] .column-right[ - Music recommendation - Suggested connections in social networks - Recommended items in e-commerce Websites - Recommended travel destinations and accommodations - ... ] --- # Common Strategies * **Popularity** - Recommend items most people like * **Item Similarity** - Recommend **items that are similar** to what the user has already shown interest * **User Similarity** - Recommend items that are preferred by **users who are similar the the target user** in some ways * **Diversity** - Recommend items that are **least known** to the uuser --- # The Long Tail
[https://www.forbes.com/sites/robinlewis/2016/05/31/the-long-tail-theory-can-be-reality-for-traditional-megabrands/#2b77afbc6372](https://www.forbes.com/sites/robinlewis/2016/05/31/the-long-tail-theory-can-be-reality-for-traditional-megabrands/#2b77afbc6372) --- class: middle, center # Content-based Recommendation --- # Content-based Recommendation * **Assumptions** - Every user has his/her own **interests** / **tastes** / **preferences** - Each user's preferences can be represented as **a summary of what he/she has seen/read/watched/liked in the past** - A user will prefer something he or she is interested in * We can compare the **content** or **characteristics** of the items * Recommend items that are **similar** to what the user has consumed before --- # Content-based Recommendation ### Two Steps 1. Learn user **preferences** (what does the user like?) 2. Find items that **match** these preferences ### Problems 1. How do we **learn** user preferences? 2. How do we **represent** user interests? 3. How do we **represent** items? 4. How to measure **similarity**? --- # Content-based Recommendation ### **Similarity-based** * **Steps** - Define features to represent the items (e.g. bag-of-words, author, publish date/time, etc.) - Construct **user profile** by the items liked by the user (e.g. average of feature vectors) - Calculate **similarity** between user profile and the new items - Return a **ranked list** of items * What is important here is the **user profile** - How can we **represent** a user? - A user may have **multiple interests**, or his/her interests may **change over time** --- # Content-based Recommendation ### Limitations of Content-based Methods * Content (including meta-data) might not be available or enough in some domains * It is difficult to represent some items by their 'content' (e.g. movies, books, music) * Content-based methods tend to return very similar items --- class: center, middle # Collaborative Filtering --- # Collaborative Filtering ### What is Collaborative Filtering (CF)? * From [Wikipedia](https://en.wikipedia.org/wiki/Collaborative_filtering):
*In the newer, narrower sense, collaborative filtering is a method of making automatic predictions (filtering) about the interests of a user by collecting preferences or taste information from many users (collaborating). The underlying assumption of the collaborative filtering approach is that if a person A has the same opinion as a person B on an issue, A is more likely to have B's opinion on a different issue than that of a randomly chosen person.* --- # Collaborative Filtering ### Basic Idea * Instead of relying on the content of the items, we can analyse people’s **tastes and preferences** * Each person is NOT totally different from another * There are different **kinds** of people, for example: - People who like action movies - People who read literature - People who like spicy food * By grouping **similar users**, we can recommend similar items to similar users * This does not require a lot of information about the users and items themselves --- # Collaborative Filtering ### Two Types of Collaborative Filtering 1. **Memory-based** - Directly use ratings from similar users or items - Also called **neighbourhood-based** methods 2. **Model-based** - Mathematical models are used to represent users, items and their relations - E.g. **matrix factorization**, Bayesian networks, probabilistic models --- # Collaborative Filtering ### User-item Interaction * In the following discussion, we assume that a user may **rate** an item on a **1 to 5** scale
--- class: center, middle # Memory-based Collaborative Filtering --- # Neighbourhood ### What is neighbourhood? * Consider again the **vector space model** * Users and items can be represented as **vectors** in a high dimensional space * More similar items/users will appear **closer** to each other
--- # Neighbourhood Models ### Two Types of Neighbourhood Models 1. **User-based** - We consider **similar users** - The neighbourhood of a user consists of users who like similar items 2. **Item-based** - We consider **similar items** - The neighbourhood of an item consists of items that are preferred by similar users --- # User-based Collaborative Filtering * **Task**: Predict the **extent** to which user `\(u\)` likes item `\(i\)` * **Procedures**: - We have user `\(u\)`, and item `\(i\)` - Find a set of users who are similar to `\(u\)` and have rated `\(i\)` - Get the **average rating** on `\(i\)` given by this set of users - Do this for all items, come up with a **ranking** based on the predict rating --- # User-based Collaborative Filtering * In doing **user-based CF**, we made the following **assumptions**: - If users had similar tastes in the past, they should have similar tastes in the future - User preferences remain **stable and consistent** over time * Furthermore, we need to define **similarity** * **Similarity** - Should reflect how **close** the tastes and preferences of two users are - Similar users should assign **similar ratings** to the same set of items --- # Similarity - Pearson Correlation * One way of computing similarity between two users is to use the **pearson correlation**
--- # Similarity - Pearson Correlation * `\(x\)`, `\(y\)`: users * `\(r_{x,i}\)`: rating assigned to `\(i\)` by `\(x\)` * `\(I\)`: the set of items rated by both `\(x\)` and `\(y\)` * `\(\text{sim}(x, y)\)` has a value between -1 and 1
--- # Similarity - Pearson Correlation * In Python, you can easily compute the correlation using the `scipy` module's [pearsonr function](https://docs.scipy.org/doc/scipy/reference/generated/scipy.stats.pearsonr.html) ```python >>> from scipy.stats import pearsonr >>> a = [5,2,1,4,3,1] >>> b = [1,5,4,2,1,2] >>> pearsonr(a,b) (-0.59628479399994383, 0.21157899460007421) >>> >>> a = [5,2,1,4,3,1] >>> b = [4,3,1,5,4,2] >>> pearsonr(a,b) (0.85978530414910515, 0.028111919656069226) >>> ``` --- # Predicting Ratings * How to **predict** a user's rating for an item? * Use the equation below:
* Example: see [l5-user-based-cf.ipynb](https://colab.research.google.com/drive/1KgSz_razs9UwFfpL0hg9K3_Fh_JqTre_) --- # Limitations * **Data sparsity** - When there are a lot of users and items, very few overlap between users * **Does not scale** - When there are 10 million users, how can you generate all their neighbourhoods? * Two users may have similar taste in one domain but very different taste in another --- # Item-based Collaborative Filtering ### Procedures * We have user `\(u\)` and item `\(i\)` * Find a set of **items**, which are - rated by `\(u\)` - given **similar ratings** as `\(i\)` by other users * Get the **average rating** of this set of items given by `\(u\)` * Use that as the predicted rating of `\(i\)` by `\(u\)` --- # Item-based Collaborative Filtering * In doing **item-based CF**, we made the following **assumptions**: - If two items are given similar ratings by the users, they should have **similar characteristics** * Consider **movies**: - Movies of the same genre, by the same director, or feature the same actor/actress will be assigned similar ratings * Ref: [Amazon.com Recommendations: Item-to-Item Collaborative Filtering](https://dl.acm.org/citation.cfm?id=642471) --- # Predicting Ratings * One way to implement item-based CF is to compute a **weighted combination of ratings** given by `\(u\)` to other items
--- # Neighbourhood-based Collaborative Filtering * Neighbourhood and recommended items are usually calculated **offline** * In order to reduce the amount of computation needed, the size of the neighbourhood is usually **limited** * Previous research shows that a neighbourhood size of **20-50** is quite enough * Ref: [Empirical Analysis of Design Choices in Neighborhood-based Collaborative Filtering Algorithms](https://dl.acm.org/citation.cfm?id=594047), Herlocker et al., 2002. --- class: center, middle # Food for Thought ### TED Talk ### How Algorithms Shape Our World #### TEDGlobal 2011, By Kevin Slavin [http://www.ted.com/talks/kevin_slavin_how_algorithms_shape_our_world.html](http://www.ted.com/talks/kevin_slavin_how_algorithms_shape_our_world.html) --- class: center, middle # Model-based Collaborative Filtering --- # Model-based Collaborative Filtering * What we have discussed so far are called **memory-based** collaborative filtering * We have not **trained** any model that can be used to describe the relationship between inputs and outputs * Memory-based models are **easy to implement**, but usually are NOT very accurate and NOT **scalable** * Instead, we can consider a **machine learning approach** to the task of recommendation: - Create a model that explains how **ratings are generated**, or how **items are ranked** - Use past data to **train/optimize** the parameters of the model --- # Model-based Collaborative Filtering ### We can roughly categorize model-based CF into two types: * **Matrix Factorization Approach** - Assume that there are **latent factors** that determine how users rate items - Decompose the user-item matrix using matrix factorization techniques * **Classification Approach** - Consider the task of recommendation as a **classification** problem - For each given pair of user and item, we determine whether the user will be interested in the item (binary classification) - Can take into account **contextual information** and **implicit feedbacks** --- class: middle, center # Gradient Descent --- # Parameter Optimization * Training machine learning models usually means **optimizing parameters** in the model using the **training data** * Each model is characterized by a set of **parameters** * Consider linear regression as an example: $$y = b_0 + b_1 x_1 + b_2 x_2 + ... + b_n x_n$$ * Each `\(b_i\)` is a parameter of the model * How exactly do we find the most suitable values of these parameters given the training data? --- # Parameter Optimization * In some cases, we can find a solution **analytically** - The solution can be represented by a equation - The best parameters can be obtained by substituting the training data `\(X\)` and `\(y\)` into the equation * However, in many cases, the model is complicated and we cannot do that analytically * Another approach: **trial and error** 1. **Initialize** the paraemeters randomly 2. Use the model to **generate predictions** for the training data 3. Computer the **error** of the predictions 4. Use the error to **adjust** the parameters 5. Go to Step 1 if model is not good enough --- class: split # Gradient Descent .column-left[ * Let's consider a very simple example * We want to learn a linear model `\(y = mx\)` * Our training data: - `X = (1, 2, 3, 4)` - `y = (2.4, 3.5, 5.5, 8.7)` * Obviously the value of `\(m\)` can be determined analytically * Let's try our **gradient descent** on this example ] .column-right[
] --- # Gradient Descent * To perform gradient descent, we need to first have an **error function** that allows us to understand how much error we are making using current values of the parameters (also called **objective function** or **loss function**) * Our error function: $$ error = \frac{1}{N} \sum_{i=1}^N (y_i - \hat{y}_i)^2 $$ $$ = \frac{1}{N} \sum_{i=1}^N (y_i - m x_i)^2 $$ * where N is number of training samples * (note that we use the **mean squared error** in this case) --- class: split # Gradient Descent .column-left[ * The objective is to **adjust** the value of our parameter `\(m\)` such that next time the error will be **smaller** * By **adjusting** we mean either **increase** or **decrease** its value * To know to which direction we should adjust `\(m\)`, we need to know the **gradient** of the error * In our case: $$ \frac{\partial e}{\partial m} = \frac{1}{N} \sum_{i=1}^N (-2 x_i y_i + 2 m x_i^2) $$ ] .column-right[
] --- class: split # Gradient Descent * Once we know the gradient, we know how to adjust `\(m\)` * If gradient is **positive**, we need to **reduce** `\(m\)` * If gradient is **negative**, we need to **increase** `\(m\)` * We use a **hyperparameter** called the **learning rate** to determine **how much** do we adjust `\(m\)` each time - If we change the value too much, we may **miss** the optimal value - If we cahnge the value too little, we may never arrive at the optimal value * Implementation in Python: [l5-gradient-descent-example.ipynb](https://colab.research.google.com/drive/1GY9jFS_iwuD-BSnr_sOmdZ7T6SbrVhGE) --- class: middle, center # Matrix Factorization --- # Model-based Collaborative Filtering * Recall that in recommender systems, we usually deal with a matrix of **user-item ratings** * In **memory-based methods**, we directly compute a prediction based on the other ratings * In **model-based methods**, we come up with a **model** of how ratings are **generated** * **Matrix factorization** is a commonly used model-based methods in recommendations
--- # Matrix Factorization - Basic Idea * We assume that users and items can be grouped into different **types** * Take **movies** as an example: - Some users like action movies, while some like romantic movies - Some movies are romantic, while some are exciting and full of suspense
--- # Matrix Factorization ### Challenge * How can we discover **types** of users and items from our data? * **Clustering**?
--- # Matrix Factorization * Clustering users and items separately **does NOT** work well - We need to **manually inspect** the meaning of each group (cluster) - We do not know which user groups correspond to which item groups - There is no guarantee that we will obtain exact **correspondence** between user groups and item groups - E.g. there might be a group of users who like animations, but animations might be grouped under different clusters according to their content --- # Matrix Factorization * We can approach this problem differently * Let's assume in advance that there are **`\(K\)` different types of users and items** * We use **vectors of length `\(K\)`** to represent users and items * Each component (**factor**) in a vector represents the **extent** to which the user/item **belongs to that type**
$$ \text{user}_1 = (0.0, 0.1, 0.2, 1.2, 2.3) \\\ \text{user}_2 = (3.1, 0.0, 0.1, 0.2, 0.4) $$ $$ \text{item}_1 = (0.2, 0.9, 1.5, 0.2, 0.8) \\\ \text{item}_2 = (1.5, 2.3, 0.0, 0.9, 0.0) $$ --- # Matrix Factorization * If we consider all the **users** and **items** in our recommender system, we can represent all of them using two different **matrices**
--- # Matrix Factorization * In such a model, the rating on item `\(i\)` given by user `\(u\)` is generated by computing the **dot product** of the corresponding user and item **vectors** * This is equivalent to multiplying the (transpose of) the item matrix with the user matrix
--- # Matrix Factorization * Usually, we are given the matrix `\(R\)`, **matrix factorization** is the process of finding `\(P\)` and `\(Q\)` such that `\(P x Q^T\)` gives an approximation of `\(R\)` $$ P \times Q^T = \hat{R} \approx R $$ * Very often `\(R\)` is **incomplete** (e.g. 99% of the cells are empty), * Therefore, we have to estimate the values in `\(P\)` and `\(Q\)`, instead of solving for exact values • The number of factors `\(K\)` reflects the complexity of our model --- class: split # Matrix Factorization .column-left[ * In matrix factorization, our target is to come up with `\(P\)` and `\(Q\)`, the two **factor matrices** whose product approximates the user-item rating matrix `\(R\)` * When we say approximate, we are talking about the **known values** in `\(R\)` * If we can approximate the known values well, our **predictions** of the unknown values will be **accurate** ] .column-right[
] --- # Matrix Factorization * Let's focus on **one rating** at a time
$$ \hat{r}\_{ui} = \sum\_{k=1}^K p\_{uk} q\_{ki} $$ --- # Matrix Factorization * Our goal is to find all `\(p_{ik}\)` and `\(q_{kj}\)` such that $$ \sum\_{k=1}^K p\_{uk} q\_{ki} \approx r\_{ui} $$ * Our data only contain the values of **some** `\(r_{ij}\)` * How can we determine the values of all `\(p_{ik}\)` and `\(q_{kj}\)`? --- # Matrix Factorization ### Basic Idea: * We first initialize `\(P\)` and `\(Q\)` with some **random values** * We measure our **error**, i.e. how far we are from the **true** values in R * We update the values in `\(P\)` and `\(Q\)` based on the error we computed * **Repeat** the steps above until the error is sufficiently small
* In other words, we can use **gradient descent** --- # Matrix Factorization * Example:
* The **dot product** of the user vector and the item vector is: $$ 0.5 \times 1 + 1 \times 0 + 1.5 \times 2 = 3.5 $$ * We can then compute our **error** --- # Matrix Factorization * Error is give by: $$ e\_{ui} = r\_{ui} - \hat{r}\_{ui} = r\_{ui} - \sum\_{k=1}^K p\_{uk} q\_{ki} $$ * Squared error: $$ e\_{ui}^2 = (r\_{ui} - \hat{r}\_{ui})^2 = (r\_{ui} - \sum\_{k=1}^K p\_{uk} q\_{ki})^2 $$ * The **machine learning** problem here is to optimize all `\(p\)`'s and `\(q\)`'s such that `\(e_{ui}^2\)` is **minimized** --- # Matrix Factorization ### Gradient Descent $$ e\_{ui}^2 = (r\_{ui} - \hat{r}\_{ui})^2 = (r\_{ui} - \sum\_{k=1}^K p\_{uk} q\_{ki})^2 $$ $$ \frac{\partial e\_{ui}^2}{\partial p\_{uk}} = -2 (r\_{ui} - \sum\_{k=1}^K p\_{uk} q\_{ki}) q\_{ki} = -2 e\_{ui} q\_{ki} $$ $$ \frac{\partial e\_{ui}^2}{\partial q\_{ki}} = -2 (r\_{ui} - \sum\_{k=1}^K p\_{uk} q\_{ki}) p\_{uk} = -2 e\_{ui} p\_{uk} $$ --- # Matrix Factorization * Having obtained the gradients, we can construct our **update rules** as follows:
$$ p'\_{uk} = p\_{uk} - \alpha (-2 e\_{ui} q\_{ki}) = p\_{uk} + 2 \alpha e\_{ui} q\_{ki} $$
$$ q'\_{ki} = q\_{ki} - \alpha (-2 e\_{ui} p\_{uk}) = q\_{ki} + 2 \alpha e\_{ui} p\_{uk} $$
* where `\(\alpha\)` is the **learning rate** * `\(p'_{uk}\)` and `\(q'_{ki}\)` are the **new values** --- # Matrix Factorization ### Training Data * Note that we only optimize `\(P\)` and `\(Q\)` using the **known values** in the matrix `\(R\)` * We can consider transforming the user-item rating matrix into a list of **tuples**:
(user, item, rating):
--- # Beyond Rating Predictions * In many other cases, we do NOT always have **ratings (explicit feedback)** from the users * Instead, we would have **implicit feedback** from the users on the items - The user purchased an item - The user clicked on an advertisement - The user viewed the details of an item * Implicit feedbacks can also be considered as **(weaker) indications** that the user is interested in the items * We can still populate a user-item matrix using implicit feedbacks * Ref: [Collaborative Filtering for Implicit Feedback Datasets](http://yifanhu.net/PUB/cf.pdf) (Hu et al. 2008) --- class: center, middle # Recommendation as Classification --- # Recommendation as Classification * Besides rating prediction using matrix factorization, recommendation can also be considered as a **classification task** * Ultimately, we want to determine the **probability that a user is interested / likes / wants to purchase an item** * Besides the explicit/implicit feedbacks, there are actually a lot of things we can consider as **features** - date/time when the users visit the Website - the browsing history of the users - the various characteristics of the items (e.g. actors/actresses in a movie, storyline of a fiction) - Whether the user is using a PC or a smartphone - **interactions** between user and item features --- # Recommendation as Classification * Recommendation can be considered as a **binary classification** problem - Whether the user will **click** on an advertisement - Whether the user will **purchase** the item - Whether the user will **download** the mobile app * **Common classification models** can be used - Logistic regression - Support vector machines - Decision trees / Random forests * The most important things in this approach are the **features** --> **Feature Engineering** --- # Recommendation as Classification * To train a classifier, you need both **positive** and **negative** samples * However, very often you don't know what the user **DOES NOT** like * A user hasn't interacted with an item DOES NOT mean that he/she is not interested in an item * **Negative sampling** - For each positive feedback you have, **randomly sample** items that the user has not interacted with - Use these items as **negative** samples - Can also weight each sample differently (how?) --- class: center, middle # End of Lecture 5


idlib.data_elements¶
DataElement¶
-
class
idlib.data_elements.
DataElement
(ui=None)[source]¶ Bases:
object
The base class for all data elements in iDISK.
- Parameters
ui (str) – The unique identifier for this data element (Optional).
-
add_elements
(elements)[source]¶ Add a collection of elements to this data element if it does not already belong to it. Each element must be an Atom, Attribute, or Relationship.
- Parameters
elements (iterable) – The elements to add.
-
get_atoms
(atom_name=None, r_type='object')[source]¶ Returns a generator over the atoms of this data element, if implemented.
- Parameters
r_type (str) – How to yield each atom. Possible values are [“object”, “dict”]. If “object”, yields Atom instances. If “dict”, yields dicts from the Atom.to_dict() method.
- Returns
generator over atoms
- Return type
generator
-
get_attributes
(atr_name=None, r_type='object')[source]¶ Returns a generator over the attributes of this data element, if implemented.
- Parameters
atr_name (str) – If not None (default), return only those attributes of type atr_name.
r_type (str) – How to yield each attribute. Possible values are [“object”, “dict”]. If “object”, yields Attribute instances. If “dict”, yields dicts from the Attribute.to_dict() method.
- Returns
generator over attributes
- Return type
generator
-
classmethod
get_instances
()[source]¶ Get all instances of the Concept class.
- Returns
Generator over Concept instances.
- Return type
generator
-
get_relationships
(rel_name=None, r_type='object')[source]¶ Returns a generator over the relationships of this concept.
- Parameters
rel_name (str) – If not None (default), return only those relationships of type rel_name.
r_type (str) – How to yield each relationship. Possible values are [“object”, “dict”]. If “object”, yields Relationship instances. If “dict”, yields dicts from the Relationship.to_dict() method.
- Returns
generator over relationships
- Return type
generator
-
classmethod
init_counter
(num)[source]¶ Initialize the unique identifier counter with the given number.
- Parameters
num (int) – The number to initialize with.
-
property
num_atoms
¶
-
rm_elements
(elements)[source]¶ Remove a collection of elements from this data element. Each element must be an Atom, Attribute, or Relationship.
- Parameters
elements (iterable) – The elements to remove.
-
classmethod
set_ui_prefix
(prefix)[source]¶ Set the string to prepend to the UI of each instance.
- Parameters
prefix (str) – The prefix to set.
-
property
ui
¶ The unique identifier is always dynamically determined by the values of self._prefix and self._number.
Atom¶
-
class
idlib.data_elements.
Atom
(term, src, src_id, term_type, is_preferred, ui=None, **attrs)[source]¶ Bases:
idlib.data_elements.DataElement
An Atom is an a unique string, source, source ID, and term type. A collection of Atoms is a Concept.
- Parameters
term (str) – The string of this atom.
src (str) – The source code of where this atom was found.
src_id (str) – The ID of this atom in its source.
term_type (str) – The type of term. E.g. “SY” for synonym.
is_preferred (bool) – Whether this string is the preferred name in its source.
ui (str) – The iDISK unique identifier of this atom. Optional.
Concept¶
-
class
idlib.data_elements.
Concept
(concept_type, atoms=None, ui=None)[source]¶ Bases:
idlib.data_elements.DataElement
An iDISK concept, which is a collection of Atoms.
- Parameters
concept_type (str) – The iDISK type of this concept. E.g. “SDSI”. See
idlib.config
.atoms (list(Atom)) – List of synonyms for this concept. Each member must be an instance of Atom. Optional.
ui (str) – the iDISK CUI for this concept. Optional.
-
classmethod
from_concept
(concept)[source]¶ Create a new Concept instance with the same Atoms, Attributes, and Relationships as this one, but with a new UI. Attributes and Relationships are copied in an analogous manner and their subjects are updated to the new UI.
- Parameters
concept (Concept) – The concept to initialize from.
- Returns
New Concept
-
classmethod
from_dict
(data)[source]¶ Creates a concept from a JSON object. The JSON object must have the format:
{"ui": str, "concept_type": str, "synonyms": [{"term": str, "src": str, "src_id": str, "term_type": str, "is_preferred": bool}, {...}] "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] "relationships": [{"rel_name": str, "object": str, "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
Note that if the “relationships” field is not empty, the subject Concepts of the resulting Relationship instances will not be properly linked. In this case, run Concept.resolve_relationships() after all Concepts have been created.
- Parameters
data (dict) – Input JSON data.
- Returns
Concept instance built from data.
- Return type
-
property
preferred_atom
¶ The preferred term for a concept is the preferred term from the highest ranking source. That is, the atom such that atom[“src”] is the closest to the lowest index of the SOURCES list and atom[“is_preferred”] is True.
If SOURCES is not defined (e.g. if no config has been loaded) then a preferred atom is chosen at random.
- Return type
-
classmethod
resolve_relationships
()[source]¶ When multiple Concept instances are created from a JSON lines file and contain relationships that reference each other, we have to wait until all concepts are created before the objects of the relationships resolved into Relationship instances from their UIs. When this is the case, this method should be run after creating all concept instances.
-
to_dict
()[source]¶ Return this concept as an OrderedDict in the iDISK JSON format.
{"ui": str, "concept_type": str, "synonyms": [{"term": str, "src": str, "src_id": str, "term_type": str, "is_preferred": bool}, {...}] "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] "relationships": [{"rel_name": str, "object": str, "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
- Returns
Dictionary in the iDISK JSON format.
- Return type
OrderedDict
Attribute¶
-
class
idlib.data_elements.
Attribute
(subject, atr_name, atr_value, src, ui=None)[source]¶ Bases:
idlib.data_elements.DataElement
An attribute of a concept or relationship.
- Parameters
subject (Concept/Relationship) – The subject of this attribute.
atr_name (str) – The name of this attribute. E.g. “has_background”.
atr_value (str) – The value of this attribute.
src (str) – The source code of where this attribute was found.
-
classmethod
from_attribute
(attribute)[source]¶ Initialize a new Attribute from the provided with the same subject Concept, atr_name, atr_value, and src, but with a new UI.
- Parameters
attribute (Attribute) – The Attribute instances to initialize from.
-
classmethod
from_dict
(data, subject)[source]¶ Create an Attribute instance from data. data must be a dict with the following format:
{"atr_name": str, "atr_value": str, "src": str}
- Parameters
data (dict) – Input dictionary
subject (Concept/Relationship) – Subject of this attribute.
- Returns
Attribute instance
- Return type
-
to_dict
(return_subject=False, verbose_subject=False)[source]¶ Output this attribute as a dictionary, optionally with a subject. The subject is optional to accord with the iDISK JSON format.
return_subject=False
{"atr_name": str, "atr_value": str, "src": str}
return_subject=True
{"subject": subject.ui, "atr_name": str, "atr_value": str, "src": str}
return_subject=True, verbose_subject=True
{"subject": str(subject), "atr_name": str, "atr_value": str, "src": str}
- Parameters
return_subject (bool) – If True, the returned dict contains a “subject” key.
verbose_subject (bool) – If True and return_subject is True, the value of the “subject” key includes the ui, name, and source, instead of just the ui.
- Returns
dictionary representation of this attribute.
- Return type
dict
Relationship¶
-
class
idlib.data_elements.
Relationship
(subject, rel_name, object, src, ui=None)[source]¶ Bases:
idlib.data_elements.DataElement
A relationship between two concepts.
- Parameters
subject (Concept) – The subject of this relationship.
rel_name (str) – The relation. E.g. “ingredient_of”.
object (Concept/str) – The object of this relationship. Can be a Concept instance or a concept UI.
src (str) – The source of this relationship, e.g. “UMLS”.
attributes (list(Attribute)) – Any attributes of this relationship.
-
classmethod
from_dict
(data, subject, concept_mapping=None)[source]¶ Create an Relationship instance from data. data must be a dict with the following format:
{"rel_name": str, "object": str, "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
- Parameters
data (dict) – Input dictionary
subject (Concept) – Subject of this relationship.
concept_mapping (dict) – Mapping from strings to concepts as {string: Concept}, where string is equal to data[“object”]. Optional. If None, the object UI is used instead of a Concept instance.
- Returns
Relationship instance
- Return type
-
classmethod
from_relationship
(relationship)[source]¶ Create a new Relationship instance initialized from the provided with the same subject, rel_name, object, and src, but with a new UI.
- Parameters
relationship (Relationshp) – The Relationship to initialize from.
- Returns
The new Relationship.
- Return type
-
get_attributes
(r_type='object', return_subject=False)[source]¶ Return a generator over attributes of this relationship.
- Parameters
str (r_type) – The type of what to yield. Possible values are [“object”, “dict”] If “object”, yields Attribute objects. If “dict”, yields dicts.
bool (return_subject) – If True, the returned dict contains a “subject” key.
- Returns
Generator over attributes
- Return type
generator
-
to_dict
(return_subject=False, verbose=False)[source]¶ Output this relationship as a dictionary, optionally with a subject. The subject is optional to accord with the iDISK JSON format.
return_subject=False
{"rel_name": str, "object": str(object.ui), "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
return_subject=True
{"subject": str(subject.ui), "rel_name": str, "object": str(object.ui), "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
return_subject=True, verbose=True
{"subject": str(subject), "rel_name": str, "object": str(object), "src": str, "attributes": [{"atr_name": str, "atr_value": str, "src": str}, {...}] }
- Parameters
return_subject (bool) – If True, the returned dict contains a “subject” key.
verbose (bool) – If True and return_subject is True, the values of the “subject” and “object” keys include the ui, name, and source, instead of just the ui.
- Returns
dictionary representation of this attribute.
- Return type
dict


| Metamath Proof Explorer Real and Complex Numbers |
||
| Mirrors > Home > MPE Home > Real and Complex Numbers |
| Contents of this page |
...my daughters have been studying (chemistry) for several
semesters, think they have learned differential and integral calculus in
school, and yet even today don't know why
x · y =
y · x is true.
—Edmund Landau |
To derive the postulates as theorems, we define each of these objects as specific sets, then derive their properties from the axioms of set theory. The derivation is not easy, but the fact that it works is quite remarkable and lends support to the idea that ZFC set theory is all we need to provide a foundation for essentially all of mathematics.
For convenience, after deriving the complex number postulates we
re-introduce them as new axioms on top of set theory.
This lets us easily identify which axioms are needed
for a particular complex number proof, without the obfuscation
of the set theory used to derive them.
To do this, we introduce two classes
` CC `
(set of complex numbers) and
` RR `
(set of real numbers); three constants
` 0 `
(zero),
` 1 `
(one), and
` _i `
(imaginary unit, that is, the square root of minus 1); two binary operations
` + `
(plus) and
` x. `
(times); and one binary relation
`
In some cases, an alias for an axiom is created so that its name
will follow other naming conventions.
In these cases, the alias is used from then on.
For example, the closure law for addition of complex numbers
(axiom 4 of 22) is proven in
axaddcl,
restated as axiom ax-addcl,
and then aliased as addcl
so its name follows closure naming conventions;
addcl is used from then on.
In these cases the axiom's comment
is marked with "(New usage is discouraged.)"
and identifies its conventional alias.
This improves consistency by
encouraging proofs to use our conventional aliases.
Many other concepts are derived from the postulates.
For example,
subtraction and division are introduced later as definitions.
We later define natural numbers, integers, and rational
numbers as specific subsets of
` CC ` ,
leading to the nice relationships
` NN `
` C. `
` ZZ `
` C. `
` QQ `
` C. `
` RR `
` C. `
` CC ` .
We later define the set of extended reals
(real numbers, positive infinity, and negative infinity), and once those
are defined, we define
the traditional relation
` < `
(less than) over the extended reals by building on the
previously-defined relation
`
The following table presents the 22 axioms for complex numbers
in the Metamath Proof Explorer,
along with some commentary about them:
In case you are wondering: Why do we use (purple) class variables
for most postulates
instead of more conventional (red) setvar variables?
The answer is simply that it's more convenient.
In fact, we can equivalently state these
with setvar variables only (which would be more in keeping with
textbook notation), and then prove these class-variable versions from them.
You may want to do that if you want a nice conventional presentation of
these axioms for your classroom, book, etc. However, in our formalism,
the advantage of a class variable is that we can directly substitute it
with another class expression such as the number "2" or the term
"` ( ( _i x. `
` x ) + `
` B ) `".
A setvar variable would require some logic manipulations to do
this, using theorems such as vtoclg (as used,
for example, to convert elirrv to
elirr).
So for convenience we use class variables outright. On the other
hand, a class variable cannot be quantified with
` A. `
(for all)
and
` E. `
(there exists),
so for axioms with quantifiers, the setvar variables are unavoidable.
The axioms and proven theorems that apply to all sets or classes
are not considered axioms for complex numbers, since they apply
in other situations as well.
For example, there are many general theorems about equality
that apply to complex numbers.
We separately prove that
` A `
` = `
` A `
in eqid.
If
` A `
` = `
` B ` ,
then
` B `
` = `
` A `
per eqcomi,
` ( A F C ) = ( B F C ) `
per oveq1i, and
` ( C F A ) = ( C F B ) `
per oveq2i.
If
` A `
` = `
` B `
and
` B `
` = `
` C ` ,
then
` A `
` = `
` C ` per
eqtri (that is, equality is transitive).
Also note that
` ( ( A = B /\ C = `
` D ) -> ( A F C ) = ( B F D ) ) `
as proven in oveq12.
From these axioms many other statements can be proven.
For example,
` 0 `
` e. `
` CC `
is proven in 0cn.
Most analysis texts construct complex numbers as ordered pairs of
reals, leading to construction-dependent properties that satisfy these
axioms but are not usually stated as explicit axioms. Other texts state
simply that " ` RR `
is a complete ordered subfield of ` CC ` ," leading to redundant axioms when this phrase is
completely expanded out.
To our knowledge, the complete set of axioms in the
exact form given here has never been published before.
That said, Slawomir Kolodynski found a reference with
27 complex number axioms, similar in spirit to Metamath's axioms:
Edward V. Huntington, "The fundamental propositions of
algebra," Monographs on Topics of Modern Mathematics Relevant to the
Elementary Field, edited by I. W. A. Young, New York, 1911; see also
Trans. Amer. Math. Soc., vol. VI, 1905, pp. 209—229.]
The original list of complex number axioms was longer.
In 2012 Eric Schmidt released
"Reductions in Norman Megill's axiom system for complex numbers",
available as schmidt-cnaxioms.pdf (schmidt-cnaxioms.tex).
This paper showed that several of the original axioms could be weakened
(as discussed above).
The paper also showed that several of the axioms of the time
were redundant (could be derived from the others), e.g., that
axaddcom (now addcom) and
ax0id (now addid1) are redundant.
Scott Fenton later formalized these results within Metamath itself
(as proofs of the redundant theorems).
Mario Carneiro on 18-Feb-2014 proved that cnex
was redundant (it can be proven that the complex numbers are a set).
Eric Schmidt presented a proof that the remaining MPE complex number axioms,
with the possible exception of ax-mulcom,
are independent of the others.
These independence proofs have not yet been formalized in Metamath.
It is currently an open question if ax-mulcom
is independent of the others.
To construct the complex numbers, we start with the finite ordinals (natural numbers) of set theory
and successively build temporary positive
integers, temporary positive rationals, temporary positive reals (based on Dedekind cuts),
temporary signed reals, and finally the actual
complex numbers. ("Temporary" means they would
not normally be used outside of the construction.) Together with the
arithmetic operations and other auxilliary sets needed at each level,
there are a total of 36 temporary definitions involved. You can look at
the Statement List starting at cnpi (click on
its "Related theorems" link) to see the theorems used for the
construction, which total 254 (including the 22 that result in the final
axioms). These theorems are, in essence, the complete formalization of
an entire 136-page book, Landau's Foundations of Analysis (a.k.a.
Grundlagen der Analysis), although the approach we use is somewhat
more modern.
In 2013 Mario Carneiro did a
major revision and cleanup of the construction. In particular, rather
than using equivalence classes as is customary for the construction
of the temporary rationals, he used only "reduced
fractions", so that the use of
the axiom of infinity is avoided until it becomes necessary for the
construction of the temporary reals.
The construction is "portable" in the sense that the final axioms
hide how they are constructed, and another construction that
develops the same axioms could be used in place of it. For
example, another common construction is to define real numbers as Cauchy
sequences of rationals instead of the Dedekind cuts that we use.
Analysis textbooks rarely if ever actually define ` +oo ` and ` -oo ` as concrete
objects. Instead, they just say that they are two "new" distinguished
elements. But we must choose specific sets in order to use set theory
to work with them. So we pick ` ~P U. CC `
(the power set of the union of the set of complex numbers) for
` +oo ` (df-pnf) and ` ~P +oo ` for ` -oo ` (df-mnf), which we can
prove are different from each other and to not belong to ` RR ` (see theorems pnfnemnf, pnfnre, and
mnfnre). Many other choices are possible too.
In spite of the seemingly awesome "size" of these two new members, they
are really nothing deeper than notational devices to make some proofs
shorter. Any theorems making use of them can be stated equivalently
without them. They provide a shorthand for saying, for example, "no
matter how large a number we pick, this series will eventually grow
larger than that number." These "infinities" have nothing to do with
the infinite cardinals of set theory—in fact one possible choice for
` -oo ` is ` { CC } ` , which is a singleton with cardinality 1!
(We didn't use this simpler choice because its justification requires
the Axiom of Regularity, whose use we prefer to avoid when possible.)
Once the extended reals are defined, we can then define
the traditional less-than operation
` < ` using the
relation
` Norman Megill's initial plan to prove that the
rational numbers are uncountable was to formalize Cantor's diagonal
argument [external] using decimal (or possibly quaternary) expansions.
However, he ran into some technical complications, such as the fact that some
numbers have two equivalent decimal representations (e.g. 0.999... = 1.000...), that would have made a
formal proof somewhat messy. So he chose another proof that is simpler
to formalize but which he believes is in the same spirit as Cantor's
diagonal proof, in the sense that it constructs a real number different
from all the numbers in a purported list of all real numbers.
Even so, the "simpler" proof is still daunting when worked out in
complete formal detail, involving some 39 lemmas. Therefore we will
first give an informal description of the proof, then describe the key
formal lemmas that lead to the final result, which is theorem ruc (or equivalently ruclem39).
The informal
argument We will start by claiming that we
can list all the reals, i.e. that there exists a function f from
` NN ` (natural
numbers) onto ` RR `
(the reals). We will then proceed to construct a real number that is
not in this purported list f(1), f(2),
f(3),... of all reals, thereby falsifying this claim.
Here is how we construct this number. We construct, in parallel, two
auxiliary sequences g(1), g(2), g(3),... and
h(1), h(2), h(3),... derived from f(1),
f(2), f(3),...
We start off by assigning:
Now, using elementary algebra, you can check that g(1) <
g(2) < g(3) < ... < h(3) < h(2)
< h(1). In addition, for each i, the interval between
g(i) and h(i) does not contain any of the
numbers f(1), f(2), f(3), ..., f(i).
This interval keeps getting smaller and smaller as i grows,
avoiding all the f(i)'s up to that point. In effect we
are constructing an interval of real numbers that are different from all
f(i)'s. This is very much like the diagonal argument, but
it is much better suited to a formal proof. Just as happens when we add
more decimals in Cantor's proof, the sequence g(1), g(2),
g(3),... gets closer and closer (converges to) to a real number
that is not in the claimed complete listing.
As i goes to infinity, the interval shrinks down to almost
nothing. What is left in this shrinking interval? Well,
g(i) and h(i) will converge towards each
other, from opposite directions, so the interval will shrink down either
to a single point or to an empty interval. It is tempting to think that
the interval will shrink down to exactly nothing, but in fact it will
not be empty, and the formal proof shows this. Specifically, it will
contain exactly one real number, which is the supremum (meaning "least
upper bound") of all values g(i). How do we know this?
Well, it results from one of the axioms for real numbers. This axiom,
shown as ax-sup above, says that the supremum of
any bounded-above set of real numbers is a real number. And the set of
values g(i) is certainly bounded from above; in fact all
of them are less than h(1) in particular.
Contrast this to the rational numbers, where the supremum axiom does
not hold. That is why this proof fails for the rational numbers, as it
should, since we can make a countable list of all rational numbers.
To give you a concrete feel for why the supremum axiom fails for
rationals, consider the infinite set of numbers 3, 3.1, 3.14, 3.141,
3.1415... Each of these numbers is a rational number. But the supremum
is pi, which is not a rational number.
In Cantor's original diagonal proof, the supremum comes into play as
follows. As you go diagonally down the list of decimal expansions of
real numbers, mismatching the list digit by digit, at each point you
will have a new rational number with one more digit (that is different
from all numbers in the list up to that point). The supremum of this
list of new rational numbers is a real number (with an infinite number of
digits after the decimal point) that is not on the list. The statement
"all decimal expansions represent real numbers," which is often stated
casually and taken for granted, is actually somewhat deep and needs the
supremum axiom for its derivation.
The formal
proof
The formal proof consists of 39 lemmas, ruclem1 through ruclem39, and the final theorem ruc.
In the formal proof, the functions f, g, and h
above are called ` F ` , ` G ` ,
and ` H ` . A
function value such as f(1) is expressed ` ( F `` 1 ) ` . A
natural number index i is usually expressed as ` A ` ; you can tell by
the hypothesis ` A e. NN ` such as ruclem18.a in ruclem26.
In the hypotheses for many of the lemmas, for example those for ruclem14, we let ` F ` be any function such that ` F : NN --> RR ` , meaning ` F ` can be any arbitrary mapping from ` NN ` into ` RR ` . We then derive additional
properties that ` F ` must
have. In particular, we will conclude that no matter what the
function ` F ` is, it
is impossible for it to map onto the set of all reals.
We also have to
construct the functions ` G ` and ` H ` ,
and doing this formally is rather involved. The purpose of the majority
of the lemmas, in fact, is simply to work out that the hypotheses of ruclem14 indeed result in functions ` G ` and ` H ` that have the
properties described in our informal argument section above.
What makes it complicated is the fact that ` G ` and ` H ` depend not only on ` F ` but on each other as well. So, we
have to construct them in parallel, and we do this using a
"sequence builder" that you can see defined in df-seq. The sequence builder takes in the
functions ` C ` and
` D ` defined in
hypotheses ruclem.1 and ruclem.2 of ruclem14, and uses them to construct a function
on ` NN ` whose
values are ordered pairs. The first member of each ordered pair
is the value of ` G `
and the second is the value of ` H ` . By using ordered pairs, the sequence builder can
make use of the previous values of both ` G ` and ` H ` simultaneously for its internal recursive
construction.
The function ` C ` , which provides the second argument or "input
sequence" for the sequence builder ` seq ` , is constructed from ` F ` as follows. Its first value
(value at 1) is the ordered pair ` <. ( ( F `` 1 ) + 1 ) , ( ( F `` 1 ) + 2 ) >. ` . This provides the
"seed" for the sequence builder, corresponding to the initial
assignment to g(1) and h(1) in the informal argument
section above. The subsequent values at 2, 3,... are just the values of ` F ` , and these feed the
recursion part of the sequence builder to generate new ordered pairs for
the values of the sequence builder at 2, 3,....
The two functions called ` 1st ` and ` 2nd ` in hypothesis ruclem.2 of ruclem14 return the first and second members,
respectively, of an ordered pair. The ` if ` operation, defined by df-if, can be thought of as a conditional
expression operator analogous to those used by computer languages. The
expression ` if ( ph , A , B ) ` can be read "if
` ph ` is true
then the expression equals ` A ` else the expression equals ` B `".
Hypotheses ruclem.3 and ruclem.4 of ruclem14 extract the first and second
members from the ordered pair values of the sequence builder
finally giving us our desired auxiliary functions
` G ` ,
and ` H `
Armed with this information, you should now compare the arithmetic
expressions in the hypothesis ruclem.2 of ruclem14 to the ones in the informal argument
section above. Hopefully you will see a resemblance, if only a very
rough one, that will provide you with a clue should you want to study
the formal proof in more depth. By the way, the assertion (conclusion)
of ruclem14 shows the first value of the
sequence builder. You can see that the ordered pair entries match
g(1) and h(1) from the informal argument section above.
Let us now look at the key lemmas for the uncountability proof.
Lemma ruclem26 shows that ` G ` has an ever-increasing set of
values, and ruclem27 shows that ` H ` has an
ever-decreasing set of values. In spite of this, the twain shall never
meet, as shown by ruclem32. Lemma ruclem34 defines the supremum ` S ` of the values of
` G `
(i.e. the supremum of its range) and shows that
the supremum is a real number. Lemma ruclem35 shows that the supremum ` S ` is always sandwiched
between ` G ` and
` H ` , whereas ruclem29 shows that this is not true for any
value of ` F ` .
Lemma ruclem36 uses these last two facts to
show that the supremum is not equal to any value of ` F ` and therefore not in the list of
real numbers provided by ` F ` . This means, as shown by ruclem37, that ` F ` cannot map onto the set of all reals.
We are now in a position to get rid of most of the hypotheses (since
their variables are no longer referenced in the assertion). In ruclem38 we eliminate all but one hypotheses of
ruclem37 by using instances of eqid. In ruclem39
we get rid of the final hypothesis (using the
weak deduction theorem dedth, involving a quite different application of
the ` if `
operator) to result in "there is no function mapping ` NN ` onto the
reals," and finally ruc converts this to the
notation for a strict dominance relation.
There are several related interesting proofs.
There are at least
aleph-one reals (aleph1re) and
irrationals (aleph1irr).
For another very different proof that the reals are uncountable, see rucALT, which follows from the exact
computation of the cardinality of reals,
rpnnen.
# Ref Expression 1 ax-resscn
` |- RR C_ CC ` 2 ax-1cn
` |- 1 e. CC `
Weakened from earlier
` 1 e. RR ` by Eric Schmidt,
11-Apr-2007; see
theorem 1re.
3 ax-icn
` |- _i e. CC ` 4 ax-addcl
` |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC ) ` 5 ax-addrcl
` |- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR ) ` 6 ax-mulcl
` |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC ) ` 7 ax-mulrcl
` |- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR ) ` 8 ax-mulcom
` |- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) ) `
It is unknown if this can be derived from the other axioms.
9 ax-addass
` |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) ) ` 10 ax-mulass
` |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) ) ` 11 ax-distr
` |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A x. ( B + C ) ) = ( ( A x. B ) + ( A x. C ) ) ) ` 12 ax-i2m1
` |- ( ( _i x. _i ) + 1 ) = 0 ` 13 ax-1ne0
` |- 1 =/= 0 ` 14 ax-1rid
` |- ( A e. `
` RR `
` -> ( A x. 1 ) = A ) `
Weakened from earlier
ax1id (now mulid1) by Eric Schmidt,
19-Jun-2012, with formalization by Scott Fenton, 4-Jan-2013
15 ax-rnegex
` |- ( A e. `
` RR -> E. x e. RR ( A + x ) = 0 ) ` 16 ax-rrecex
` |- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR `
` ( A x. x ) = 1 ) ` 17 ax-cnre
` |- ( A e. `
` CC -> E. x e. RR E. y e. `
` RR A = ( x + ( _i x. y ) ) ) ` 18 ax-pre-lttri
` |- ( ( A e. RR /\ B e. `
` RR ) -> ( A 19 ax-pre-lttrn
` |- ( ( A e. RR /\ B e. `
` RR /\ C e. RR ) -> ( ( A 20 ax-pre-ltadd
` |- ( ( A e. RR /\ B e. `
` RR /\ C e. RR ) -> ( A 21 ax-pre-mulgt0
` |- ( ( A e. RR /\ B e. `
` RR ) -> ( ( 0 22 ax-pre-sup
` |- ( ( A C_ `
` RR /\ A =/= (/) /\ E. x e. RR A. y e. A y
Past Work
Ref
Expression axcnex
` |- CC e. _V `
Proved redundant by Mario Carneiro on 18-Feb-2014; see
theorem cnex
axaddcom
` |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) ) `
Proved redundant by Eric Schmidt, 19-Jun-2012,
and formalized by Scott Fenton on 4-Jan-2013; see
theorem addcom.
ax0id
` |- ( A e. `
` CC -> ( A + 0 ) = A ) `
Proved redundant by Eric Schmidt, 19-Jun-2012,
and formalized by Scott Fenton on 4-Jan-2013; see
theorem addid1
axnegex
` |- ( A e. `
` CC -> E. x e. CC ( A + x ) = 0 ) `
Proved redundant by Eric Schmidt, 21-May-2007; see
theorem cnegex
axrecex
` |- ( ( A e. CC /\ `
` A =/= 0 ) -> E. x e. CC ( A x. x ) = 1 ) `
Proved redundant by Eric Schmidt, 21-May-2007; see
theorem recex
ax0re
` |- 0 e. RR `
Proved redundant on 19-Feb-2005; see
theorem 0re
Construction
The Extended Real Number
System A convenient device used in most
analysis texts is an extension ` RR* ` of the real number system (see df-xr and related theorems) that includes ` +oo ` and ` -oo ` .
The Real Numbers are Uncountable
In mathematics, a countable set is a set with the same cardinality
(number of elements) as the set (or some subset) of the natural numbers.
A countable set may be infinite, but every element of the set can be
mapped to a unique natural number.
The natural numbers and the integers are countably infinite sets.
Even the rational numbers are a countably infinite set; see
qnnen.
In contrast, the real numbers are not a countable set, but instead,
they are an uncountable set.
This is a remarkable result.
The question is, how can this be proved in Metamath?
g(1) = f(1) + 1
Given g(i) and h(i), we construct the next
value g(i+1) and h(i+1) as follows:
h(1) = f(1) + 2
If g(i) < f(i+1) < h(i),
then assign
In either case, f(i+1) will not fall
between g(i+1) and h(i+1).
g(i+1) =
(2` x. ` f(i+1)
+ h(i)) / 3
Otherwise, assign
h(i+1) = (f(i+1) +
2` x. ` h(i))
/ 3
g(i+1) =
(2` x. ` g(i)
+ h(i)) / 3
h(i+1) = (g(i) +
2` x. ` h(i))
/ 3
This page was last updated on 21-Aug-2020.
Copyright terms:
Public domain
W3C HTML validation
[external]